Commit 2025-02-11 00:51 d369364d

View on Github →

chore(Algebra/Group): process porting notes (#21640)

Estimated changes

Modified Mathlib/Algebra/Group/Action/Defs.lean

Modified Mathlib/Algebra/Group/Action/End.lean

Modified Mathlib/Algebra/Group/Action/Pi.lean

Modified Mathlib/Algebra/Group/Aut.lean

added theorem AddAut.neg_conj_apply

Modified Mathlib/Algebra/Group/Center.lean

Modified Mathlib/Algebra/Group/Conj.lean

Modified Mathlib/Algebra/Group/Equiv/Defs.lean

Modified Mathlib/Algebra/Group/Idempotent.lean

Modified Mathlib/Algebra/Group/Indicator.lean

Modified Mathlib/Algebra/Group/Int/Units.lean

Modified Mathlib/Algebra/Group/Nat/Even.lean

Modified Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

Modified Mathlib/Algebra/Group/Subgroup/Basic.lean

Modified Mathlib/Algebra/Group/Subgroup/Defs.lean

modified theorem Subgroup.coe_zpow

Modified Mathlib/Algebra/Group/Subgroup/Finite.lean

Modified Mathlib/Algebra/Group/Subgroup/Pointwise.lean

Modified Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean

Modified Mathlib/Algebra/Group/Submonoid/Defs.lean

Modified Mathlib/Algebra/Group/Submonoid/Operations.lean

Modified Mathlib/Algebra/Group/Submonoid/Pointwise.lean

Modified Mathlib/Algebra/Group/ULift.lean

Modified Mathlib/Algebra/Group/UniqueProds/Basic.lean

Modified Mathlib/Algebra/Group/Units/Basic.lean

Modified Mathlib/Algebra/Group/Units/Defs.lean

Modified Mathlib/Algebra/Group/WithOne/Basic.lean

Modified Mathlib/Algebra/Group/WithOne/Defs.lean

Modified Mathlib/Algebra/MonoidAlgebra/Defs.lean