Skip to content

Commit fbced36

Browse files
fix(LinearAlgebra/Matrix/Notation): fix defeq abuse in lemma (#42089)
Co-authored-by: alreadydone <3064145+alreadydone@users.noreply.github.com>
1 parent 54554e9 commit fbced36

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/LinearAlgebra/Matrix/Notation.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -401,7 +401,7 @@ section Submatrix
401401

402402
@[simp]
403403
theorem submatrix_empty (A : Matrix m' n' α) (row : Fin 0 → m') (col : o' → n') :
404-
submatrix A row col = ![] :=
404+
submatrix A row col = of ![] :=
405405
empty_eq _
406406

407407
set_option backward.isDefEq.respectTransparency false in

0 commit comments

Comments
 (0)