Commit 2020-06-01 09:01 9172cdf8

View on Github →

feat(linear_algebra/affine_space): affine spaces (#2816) Define (very minimally) affine spaces (as an abbreviation for add_torsor in the case where the group is a vector space), affine subspaces, the affine span of a set of points and affine maps.

Estimated changes

Created src/linear_algebra/affine_space.lean

added theorem affine_map.coe_mk

added def affine_map.comp

added theorem affine_map.comp_apply

added theorem affine_map.ext

added def affine_map.id

added theorem affine_map.id_apply

added theorem affine_map.map_vadd

added theorem affine_map.map_vsub

added theorem affine_map.to_fun_eq_coe

added structure affine_map

added theorem affine_space.mem_span_points

added def affine_space.span_points

added theorem affine_space.span_points_nonempty_of_nonempty

added theorem affine_space.vadd_mem_span_points_of_mem_span_points_of_mem_vector_span

added def affine_space.vector_span

added theorem affine_space.vsub_mem_vector_span_of_mem_span_points_of_mem_span_points

added def affine_space

added def affine_span

added theorem affine_span_coe

added theorem affine_span_mem

added theorem affine_subspace.mem_coe

added theorem affine_subspace.mem_univ

added def affine_subspace.univ

added theorem affine_subspace.univ_coe

added structure affine_subspace