basis): add lemma `affine_basis.linear_combination_coord_eq_self` (#13763)

Commit

3 years ago

feat(linear_algebra/affine_space/basis): add lemma `affine_basis.linear_combination_coord_eq_self` (#13763) Formalized as part of the Sphere Eversion project.

Author

ocfnash

Parents

b063c286

mathlib3 4113e00a - feat(linear_algebra/affine_space/basis): add lemma `affine_basis.linear_combination_coord_eq_self` (#13763)

mathlib3
4113e00a - feat(linear_algebra/affine_space/basis): add lemma `affine_basis.linear_combination_coord_eq_self` (#13763)