Def Commute

Modification history

2024-05-18 16:15

Mathlib/Algebra/Group/Commute/Defs.lean

chore: Delete `Algebra.GroupPower.Basic`, `Algebra.GroupWithZero.Bitwise` (#11855) …

Modified Commute View on Github →

2023-08-10 19:52

Mathlib/Algebra/Group/Commute.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified Commute View on Github →

2022-10-14 00:13

Mathlib/Algebra/Group/Commute.lean

feat: replace Algebra/Group/{Defs,Basic} with direct ports from mathlib3 (#457) …

Added Commute View on Github →