Theorem mul_right_comm
Modification history
2024-09-14 09:22
Mathlib/Algebra/Group/Basic.lean
refactor: make `(Left|Right)Commutative` typeclasses (#16751) …
Modified mul_right_commView on Github →2022-10-14 00:13
Mathlib/Algebra/Group/Basic.lean
feat: replace Algebra/Group/{Defs,Basic} with direct ports from mathlib3 (#457) …
Modified mul_right_commView on Github →