test

cadake · Oct 7, 2024 · 082a1df · 082a1df
1 parent cdddda5
commit 082a1df
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/LeanTQI/VectorNorm.lean b/LeanTQI/VectorNorm.lean
@@ -811,6 +811,7 @@ theorem lpnorm_continuous_at_p (A : Matrix m n 𝕂) :
       have : Fact (1 ≤ p) := {out := pin.left}
       exact lpnorm_rpow_ne0 p A (fun h' => h ((lpnorm_eq0_iff p A).mp h')) pin.right
 
+-- test