feat(linear_algebra/basis): add basis.ext_elem_iff (#18155)
Replace the lemma
```lean
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:
```lean
theorem basis.ext_elem_iff (b : basis ι R M) {x y : M} : x = y ↔ ∀ i, b.repr x i = b.repr y i :=
```
