Theorem Equiv.mulRight_one

Modification history

2025-02-25 16:16
Mathlib/GroupTheory/Perm/Basic.lean
chore: separate the automorphism groups from their tautological action (#22141) …
Deleted Equiv.mulRight_oneView on Github →
2023-02-28 20:37
Mathlib/GroupTheory/Perm/Basic.lean
feat: add to_additive linter checking whether additive decl exists (#1881) …
Modified Equiv.mulRight_oneView on Github →
2023-02-05 11:33
Mathlib/GroupTheory/Perm/Basic.lean
fix: use `to_additive (attr := _)` here and there (#2073)
Modified Equiv.mulRight_oneView on Github →
2023-01-06 16:39
Mathlib/GroupTheory/Perm/Basic.lean
feat: `mulLeft` is a monoid hom (#1348) …
Added Equiv.mulRight_oneView on Github →