Commit 2021-10-14 18:49 72789f57

View on Github →

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.

Estimated changes

Modified src/algebra/add_torsor.lean

added theorem set.mem_vsub

Modified src/linear_algebra/affine_space/affine_map.lean

added theorem affine_map.image_vsub_image

Modified src/linear_algebra/affine_space/affine_subspace.lean

added theorem affine_equiv.span_eq_top_iff

added theorem affine_map.map_top_of_surjective

added theorem affine_map.span_eq_top_of_surjective

added theorem affine_map.vector_span_image_eq_submodule_map

added def affine_subspace.map

added theorem affine_subspace.map_bot

added theorem affine_subspace.map_coe

added theorem affine_subspace.map_direction

added theorem affine_subspace.map_span