Commit 2023-01-15 20:09 f15389d9

feat(linear_algebra/basis): add basis.ext_elem_iff (#18155) Replace the lemma

theorem basis.ext_elem  (b : basis ι R M) {x y : M}  (h : ∀ i, b.repr x i = b.repr y i) : x = y := 

by an iff version:

theorem basis.ext_elem_iff  (b : basis ι R M) {x y : M}  : x = y  ↔ ∀ i, b.repr x i = b.repr y i :=