Theorem Equiv.mulLeft_one

Modification history

2023-02-28 20:37
Mathlib/GroupTheory/Perm/Basic.lean
feat: add to_additive linter checking whether additive decl exists (#1881) …
Modified Equiv.mulLeft_oneView on Github →
2023-02-05 11:33
Mathlib/GroupTheory/Perm/Basic.lean
fix: use `to_additive (attr := _)` here and there (#2073)
Modified Equiv.mulLeft_oneView on Github →
2023-01-06 16:39
Mathlib/GroupTheory/Perm/Basic.lean
feat: `mulLeft` is a monoid hom (#1348) …
Added Equiv.mulLeft_oneView on Github →