mathlib3

211bf1ab - feat(linear_algebra/affine_space/affine_subspace): `map_eq_bot_iff` (#16285)

feat(linear_algebra/affine_space/affine_subspace): `map_eq_bot_iff` (#16285) Add the lemma that the image of an affine subspace under an affine map is `⊥` if and only if that subspace is `⊥`.