Commit 2024-02-22 12:56 563fbc18

feat: cyclic group lemmas (#10832)

• Add a lemma stating that non-identity element of a finite group of prime order generates the group (stated in 4 ways)
• Use this to golf isCyclic_of_prime_card
• Add a version of isUnit_iff_exists_inv for non-commutative monoids.