Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-28 10:11 0c1d80f5

View on Github →

feat(linear_algebra/orientation): add orientation.reindex (#19236)

Estimated changes

Modified src/linear_algebra/alternating.lean

added theorem alternating_map.dom_dom_congr_smul

added def alternating_map.dom_dom_lcongr

added theorem alternating_map.dom_dom_lcongr_refl

added theorem alternating_map.dom_dom_lcongr_to_add_equiv

Modified src/linear_algebra/determinant.lean

added theorem basis.det_reindex'

Modified src/linear_algebra/orientation.lean

added theorem basis.orientation_reindex

added def orientation.reindex

added theorem orientation.reindex_apply

added theorem orientation.reindex_refl

added theorem orientation.reindex_symm