Theorem MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply

Modification history

2026-03-23 15:54

Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

chore(GroupTheory/SpecificGroups/Cyclic/Basic): refactor (#36983) …

Modified MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply View on Github →

2025-01-12 20:22

Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

feat(GroupTheory/SpecificGroups/Cyclic): Actions on cyclic groups factor through `ZMod` (#20359) …

Added MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply View on Github →