Def DistribMulAction.toAddEquiv₀

Modification history

2024-10-25 05:50

Mathlib/Algebra/GroupWithZero/Action/Defs.lean

chore(Algebra/GroupWithZero/Action): reduce theory included with `Group.Action.Defs` (#18190) …

Modified DistribMulAction.toAddEquiv₀ View on Github →

2024-08-19 08:56

Mathlib/Algebra/GroupWithZero/Action/Defs.lean

chore(GroupTheory/GroupAction/Group): Delete (#15806) …

Modified DistribMulAction.toAddEquiv₀ View on Github →

2023-09-21 17:41

Mathlib/GroupTheory/GroupAction/Group.lean

feat: the Unfolding Trick (#6223) …

Added DistribMulAction.toAddEquiv₀ View on Github →