Theorem Nontrivial.of_not_isCyclic

Modification history

2026-03-23 15:54
Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
chore(GroupTheory/SpecificGroups/Cyclic/Basic): refactor (#36983) …
Modified Nontrivial.of_not_isCyclicView on Github →
2023-11-29 07:29
Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
feat(GroupTheory/SpecificGroups/Cyclic): Add non-cyclic -> nontrivial (#8693) …
Added Nontrivial.of_not_isCyclicView on Github →