Theorem MulAction.IsPretransitive.of_smul_eq

Modification history

2024-05-24 03:47

Mathlib/Algebra/Group/Action/Defs.lean

chore: Move `MulAction` to under `Algebra` (#13140) …

Modified MulAction.IsPretransitive.of_smul_eq View on Github →

2024-01-23 00:50

Mathlib/GroupTheory/GroupAction/Defs.lean

feat(GroupTheory/GroupAction/Defs): `isPretransitive_of_compHom` (#9122) …

Added MulAction.IsPretransitive.of_smul_eq View on Github →