Commit 2023-11-14 14:30 fc881b75

View on Github →

refactor: Int.negOnePow as a map to ℤˣ rather than ℤ (#8307) Following #7866, Int.negOnePow is redefined as a map ℤ → ℤˣ rather than ℤ → ℤ.

Estimated changes

Modified Mathlib/Algebra/GroupPower/NegOnePow.lean

modified def Int.negOnePow

deleted theorem Int.negOnePow_mul_self

Modified Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

added theorem CochainComplex.HomComplex.Cochain.smul_v

added theorem CochainComplex.HomComplex.Cochain.units_smul_v

deleted theorem CochainComplex.HomComplex.Cochain.zsmul_v

added theorem CochainComplex.HomComplex.Cocycle.coe_smul

deleted theorem CochainComplex.HomComplex.Cocycle.coe_zsmul

modified def CochainComplex.HomComplex.δ_hom

added theorem CochainComplex.HomComplex.δ_smul

modified theorem CochainComplex.HomComplex.δ_zero

deleted theorem CochainComplex.HomComplex.δ_zsmul

Modified Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean

Modified Mathlib/Algebra/Module/Basic.lean

Modified Mathlib/CategoryTheory/Linear/Basic.lean

added theorem CategoryTheory.Linear.comp_units_smul

added theorem CategoryTheory.Linear.units_smul_comp

Modified Mathlib/CategoryTheory/Linear/LinearFunctor.lean

added theorem CategoryTheory.Functor.map_units_smul

Modified Mathlib/CategoryTheory/Triangulated/TriangleShift.lean