feat(data/zmod/quotient): Version of order_eq_card_zpowers in terms…

… of `nat.card` without a `fintype`/`finite` assumption (#16175) This PR adds a version of `order_eq_card_zpowers` in terms of `nat.card` without a `fintype`/`finite` assumption.
leanprover-community · Aug 25, 2022 · 3d0bb87 · 3d0bb87
1 parent b625803
commit 3d0bb87
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 1 deletion.
diff --git a/src/data/zmod/quotient.lean b/src/data/zmod/quotient.lean
@@ -160,4 +160,12 @@ by rw [←fintype.of_equiv_card (orbit_zpowers_equiv a b), zmod.card]
   exact fintype.card_ne_zero,
 end⟩
 
+/-- See also `order_eq_card_zpowers`. -/
+@[to_additive add_order_eq_card_zmultiples' "See also `add_order_eq_card_zmultiples`."]
+lemma _root_.order_eq_card_zpowers' : order_of a = nat.card (zpowers a) :=
+begin
+  have := nat.card_congr (mul_action.orbit_zpowers_equiv a (1 : α)),
+  rwa [nat.card_zmod, orbit_subgroup_one_eq_self, eq_comm] at this,
+end
+
 end mul_action
diff --git a/src/group_theory/order_of_element.lean b/src/group_theory/order_of_element.lean
@@ -616,7 +616,8 @@ end
 
 variables [fintype G]
 
-@[to_additive add_order_eq_card_zmultiples]
+/-- See also `order_eq_card_zpowers'`. -/
+@[to_additive add_order_eq_card_zmultiples "See also `add_order_eq_card_zmultiples'`."]
 lemma order_eq_card_zpowers : order_of x = fintype.card (zpowers x) :=
 (fintype.card_fin (order_of x)).symm.trans (fintype.card_eq.2 ⟨fin_equiv_zpowers x⟩)