mathlib
69c07a4b - feat(linear_algebra/linear_pmap): `mk_span_singleton` of the same point (#14029)

Commit

3 years ago

feat(linear_algebra/linear_pmap): `mk_span_singleton` of the same point (#14029) One more lemma about `mk_span_singleton'` and slightly better lemma names.

Author

YaelDillies

Parents

6a5d17ee

mathlib 69c07a4b - feat(linear_algebra/linear_pmap): `mk_span_singleton` of the same point (#14029)

mathlib
69c07a4b - feat(linear_algebra/linear_pmap): `mk_span_singleton` of the same point (#14029)