Commit 2023-09-06 09:06 d9573627

View on Github →

feat(linear_algebra/orientation): add orientation.reindex (#6889) This forward-ports leanprover-community/mathlib#19236

Estimated changes

Modified Mathlib/LinearAlgebra/Alternating.lean

added theorem AlternatingMap.domDomCongr_smul

added def AlternatingMap.domDomLcongr

added theorem AlternatingMap.domDomLcongr_refl

added theorem AlternatingMap.domDomLcongr_toAddEquiv

Modified Mathlib/LinearAlgebra/Determinant.lean

added theorem Basis.det_reindex'

Modified Mathlib/LinearAlgebra/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