Commit 2024-08-19 08:56 83334136

View on Github →

chore(GroupTheory/GroupAction/Group): Delete (#15806) All lemmas can be moved to earlier files

Estimated changes

Modified Mathlib.lean

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

added theorem Commute.smul_left_iff₀

added theorem Commute.smul_right_iff₀

added def DistribMulAction.toAddEquiv₀

added def Equiv.smulRight

added theorem eq_inv_smul_iff₀

added theorem inv_smul_eq_iff₀

added theorem inv_smul_smul₀

added theorem smul_eq_zero_iff_eq

added theorem smul_inv_smul₀

added theorem smul_ne_zero_iff_ne

Modified Mathlib/Algebra/GroupWithZero/Action/Prod.lean

Modified Mathlib/Algebra/GroupWithZero/Action/Units.lean

added theorem IsUnit.smul_eq_zero

Modified Mathlib/Algebra/Module/Basic.lean

Modified Mathlib/Algebra/Order/Module/Defs.lean

Modified Mathlib/Algebra/Order/Module/OrderedSMul.lean

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

Modified Mathlib/Data/Finsupp/Basic.lean

Modified Mathlib/Data/Set/Pointwise/SMul.lean

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

Deleted Mathlib/GroupTheory/GroupAction/Group.lean

deleted theorem Commute.smul_left_iff₀

deleted theorem Commute.smul_right_iff₀

deleted def DistribMulAction.toAddEquiv₀

deleted def Equiv.smulRight

deleted theorem IsUnit.smul_eq_zero

deleted theorem eq_inv_smul_iff₀

deleted theorem inv_smul_eq_iff₀

deleted theorem inv_smul_smul₀

deleted theorem smul_eq_zero_iff_eq

deleted theorem smul_inv_smul₀

deleted theorem smul_ne_zero_iff_ne