Skip to content

Commit 5b3f719

Browse files
committed
fix(LinearAlgebra/Matrix/Notation): fix defeq abuse in lemmas (leanprover-community#42090)
1 parent 671e552 commit 5b3f719

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

Mathlib/LinearAlgebra/Matrix/Notation.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -228,7 +228,7 @@ section ColRow
228228
variable {ι : Type*}
229229

230230
@[simp]
231-
theorem replicateCol_empty (v : Fin 0 → α) : replicateCol ι v = vecEmpty :=
231+
theorem replicateCol_empty (v : Fin 0 → α) : replicateCol ι v = of vecEmpty :=
232232
empty_eq _
233233

234234
set_option backward.isDefEq.respectTransparency false in
@@ -368,7 +368,7 @@ section VecMulVec
368368
variable [NonUnitalNonAssocSemiring α]
369369

370370
@[simp]
371-
theorem empty_vecMulVec (v : Fin 0 → α) (w : n' → α) : vecMulVec v w = ![] :=
371+
theorem empty_vecMulVec (v : Fin 0 → α) (w : n' → α) : vecMulVec v w = of ![] :=
372372
empty_eq _
373373

374374
@[simp]

0 commit comments

Comments
 (0)