Commit 2023-03-30 08:13 abb3db38

View on Github →

feat: port LinearAlgebra.AffineSpace.Pointwise (#3132)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean

added theorem AffineSubspace.coe_pointwise_vadd

added theorem AffineSubspace.map_pointwise_vadd

added theorem AffineSubspace.pointwise_vadd_bot

added theorem AffineSubspace.pointwise_vadd_direction

added theorem AffineSubspace.pointwise_vadd_eq_map

added theorem AffineSubspace.pointwise_vadd_span

added theorem AffineSubspace.vadd_mem_pointwise_vadd_iff