Commit 2021-12-18 16:15 47c676ed

View on Github →

feat(linear_algebra/affine_space/affine_subspace): affine_subspace.comap (#10795) This copies a handful of lemmas from group_theory/subgroup/basic.lean to get things started.

Estimated changes

Modified src/geometry/euclidean/circumcenter.lean

Modified src/linear_algebra/affine_space/affine_subspace.lean

added theorem affine_subspace.coe_comap

added theorem affine_subspace.coe_injective

added theorem affine_subspace.coe_map

added def affine_subspace.comap

added theorem affine_subspace.comap_comap

added theorem affine_subspace.comap_id

added theorem affine_subspace.comap_inf

added theorem affine_subspace.comap_mono

added theorem affine_subspace.comap_supr

added theorem affine_subspace.comap_top

deleted theorem affine_subspace.ext

added theorem affine_subspace.gc_map_comap

added theorem affine_subspace.le_comap_map

deleted theorem affine_subspace.map_coe

added theorem affine_subspace.map_comap_le

added theorem affine_subspace.map_id

added theorem affine_subspace.map_le_iff_le_comap

added theorem affine_subspace.map_map

added theorem affine_subspace.map_sup

added theorem affine_subspace.map_supr

added theorem affine_subspace.mem_comap

added theorem affine_subspace.mem_map