Commit 2023-10-02 07:53 d36df78d

View on Github →

chore(LinearAlgebra/Alternating): split (#7448) I'm going to refactor/expand API about domCoprod, and I don't want to rebuild the whole library when I do it.

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/LinearAlgebra/Alternating.lean to Mathlib/LinearAlgebra/Alternating/Basic.lean

deleted def AlternatingMap.domCoprod'

deleted theorem AlternatingMap.domCoprod'_apply

deleted def AlternatingMap.domCoprod.summand

deleted theorem AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero

deleted theorem AlternatingMap.domCoprod.summand_eq_zero_of_smul_invariant

deleted theorem AlternatingMap.domCoprod.summand_mk''

deleted def AlternatingMap.domCoprod

deleted theorem AlternatingMap.domCoprod_coe

modified theorem AlternatingMap.domDomCongr_refl

modified def AlternatingMap.domDomLcongr

deleted theorem Equiv.Perm.ModSumCongr.swap_smul_involutive

deleted theorem MultilinearMap.domCoprod_alternization

deleted theorem MultilinearMap.domCoprod_alternization_coe

deleted theorem MultilinearMap.domCoprod_alternization_eq

Created Mathlib/LinearAlgebra/Alternating/DomCoprod.lean

added def AlternatingMap.domCoprod'

added theorem AlternatingMap.domCoprod'_apply

added def AlternatingMap.domCoprod.summand

added theorem AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero

added theorem AlternatingMap.domCoprod.summand_eq_zero_of_smul_invariant

added theorem AlternatingMap.domCoprod.summand_mk''

added def AlternatingMap.domCoprod

added theorem AlternatingMap.domCoprod_coe

added theorem Equiv.Perm.ModSumCongr.swap_smul_involutive

added theorem MultilinearMap.domCoprod_alternization

added theorem MultilinearMap.domCoprod_alternization_coe

added theorem MultilinearMap.domCoprod_alternization_eq

Modified Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/Determinant.lean

Modified Mathlib/Topology/Algebra/Module/Alternating.lean