From 082a1dfd5ed452b7a64e3de0dbecdc338bebb882 Mon Sep 17 00:00:00 2001
From: root <root@LAPTOP-J47R87FF>
Date: Mon, 7 Oct 2024 13:00:26 +0800
Subject: [PATCH] test

---
 LeanTQI/VectorNorm.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/LeanTQI/VectorNorm.lean b/LeanTQI/VectorNorm.lean
index 661cbd6..33956e7 100755
--- 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