Commit 2023-11-20 10:21 01a486f7

View on Github →

chore(LinearAlgebra/AffineSpace/AffineSubspace): trivial affine morphisms (#8434) We already have the LinearEquiv versions of these. This also copies the lemmas around the definition

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean

added theorem AffineEquiv.coe_ofEq_apply

added def AffineEquiv.ofEq

added theorem AffineEquiv.ofEq_rfl

added theorem AffineEquiv.ofEq_symm

added theorem AffineSubspace.coe_inclusion_apply

added def AffineSubspace.inclusion

added theorem AffineSubspace.inclusion_rfl

added def AffineSubspace.topEquiv