Commit 2022-05-30 22:37 e7cc0eba
View on Github →feat(group_theory/perm/cycle): improve doc and namespace for cauchy's theorem (#14471) Fix a few things in the module docstring, remove namespace, add an additive version and add docstrings for Cauchy's theorem. https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Existence.20of.20elements.20of.20order.20p.20in.20a.20group/near/284399583