Commit 2021-12-18 16:15 915e2b5b

View on Github →

feat(linear_algebra/orientation): add orientation.map (#10815) This also adds alternating_map.dom_lcongr following the naming established by finsupp.dom_lcongr.

Estimated changes

Modified src/linear_algebra/alternating.lean

modified theorem alternating_map.comp_linear_equiv_eq_zero_iff

added def alternating_map.dom_lcongr

added theorem alternating_map.dom_lcongr_refl

added theorem alternating_map.dom_lcongr_symm

added theorem alternating_map.dom_lcongr_trans

Modified src/linear_algebra/orientation.lean

added def orientation.map

added theorem orientation.map_apply

added theorem orientation.map_refl

added theorem orientation.map_symm