mathlib
72789f57 - feat(linear_algebra/affine_space/affine_subspace): add lemma `affine_equiv.span_eq_top_iff` (#9695)

Commit
4 years ago
feat(linear_algebra/affine_space/affine_subspace): add lemma `affine_equiv.span_eq_top_iff` (#9695) Together with supporting lemmas. Formalized as part of the Sphere Eversion project.
Author
Parents
Loading