fix(topology/algebra/matrix): correct a lemma name (#13640)

leanprover-community · Apr 23, 2022 · 44a05db · 44a05db
1 parent 09eb35f
commit 44a05db
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/topology/algebra/matrix.lean b/src/topology/algebra/matrix.lean
@@ -72,7 +72,7 @@ lemma continuous.matrix_row {A : X → n → R} (hA : continuous A) : continuous
 continuous_matrix $ λ i j, (continuous_apply _).comp hA
 
 @[continuity]
-lemma continuous_matrix.diagonal [has_zero R] [decidable_eq n] {A : X → n → R} (hA : continuous A) :
+lemma continuous.matrix_diagonal [has_zero R] [decidable_eq n] {A : X → n → R} (hA : continuous A) :
   continuous (λ x, diagonal (A x)) :=
 continuous_matrix $ λ i j, ((continuous_apply i).comp hA).if_const _ continuous_zero