cardinality of Submonoid.powers

LeanCamCombi/Mathlib/Data/Nat/Lattice.lean

@@ -3,14 +3,10 @@ import Mathlib.Data.Nat.Lattice
 namespace Nat
 variable {ι : Sort*}
 
-@[simp]
-lemma iInf_empty [IsEmpty ι] (f : ι → ℕ) : (⨅ i : ι, f i) = 0 := by
-  rw [iInf, Set.range_eq_empty, sInf_empty]
-
 @[simp]
 lemma iInf_const_zero : (⨅ i : ι, 0) = 0 := by
   cases isEmpty_or_nonempty ι
-  · exact iInf_empty _
+  · exact iInf_of_empty _
   · exact ciInf_const
 
 end Nat

LeanCamCombi/Mathlib/Data/Set/Finite.lean

@@ -1,5 +1,13 @@
 import Mathlib.Data.Set.Finite
 
+namespace Set
+variable {α β : Type*} {s : Set α} {t : Set β}
+
+lemma Finite.of_surjOn (f : α → β) (hf : SurjOn f s t) (hs : s.Finite) : t.Finite :=
+  (hs.image _).subset hf
+
+end Set
+
 namespace Set
 variable {α : Type*} [Infinite α] {s : Set α}
 

LeanCamCombi/Mathlib/Data/ZMod/Quotient.lean

@@ -1,23 +1,11 @@
 import Mathlib.Data.ZMod.Quotient
 import LeanCamCombi.Mathlib.SetTheory.Cardinal.Finite
+import LeanCamCombi.Mathlib.GroupTheory.Subgroup.Basic
 
 open Function Set Subgroup Submonoid
 
 variable {α : Type*}
 
-section LeftCancelMonoid
-variable [LeftCancelMonoid α] {a : α}
-
--- @[to_additive (attr := simp) finite_multiples] lemma finite_powers :
---   (powers a : set α).finite ↔ is_of_fin_order a :=
--- ⟨λ h, of_not_not $ λ h', infinite_range_of_injective (injective_pow_iff_not_is_of_fin_order.2 h')
---   h, is_of_fin_order.finite_powers⟩
--- @[to_additive (attr := simp) infinite_zmultiples] lemma infinite_powers :
---   (powers a : set α).infinite ↔ ¬ is_of_fin_order a :=
--- finite_powers.not
-
-end LeftCancelMonoid
-
 section Group
 variable [Group α] {s : Subgroup α} (a : α)
 
@@ -32,17 +20,16 @@ variable {a}
 @[to_additive (attr := simp) finite_zmultiples]
 lemma finite_zpowers : (zpowers a : Set α).Finite ↔ IsOfFinOrder a := by
   simp only [← orderOf_pos_iff, ← Nat.card_zpowers, Nat.card_pos, ← SetLike.coe_sort_coe,
-    Set.nonempty_of_nonempty_subtype, Nat.card_pos_iff, Set.finite_coe_iff]
-  sorry
+    nonempty_coe_sort, Nat.card_pos_iff, Set.finite_coe_iff, Subgroup.nonempty, true_and]
 
 @[to_additive (attr := simp) infinite_zmultiples]
 lemma infinite_zpowers : (zpowers a : Set α).Infinite ↔ ¬IsOfFinOrder a := finite_zpowers.not
 
 @[to_additive IsOfFinAddOrder.finite_zmultiples']
 protected alias ⟨_, IsOfFinOrder.finite_zpowers'⟩ := finite_zpowers
 
-@[to_additive add_order_of_le_card]
-lemma orderOf_le_card (hs : (s : Set α).Finite) (ha : a ∈ s) : orderOf a ≤ Nat.card s := by
+@[to_additive]
+lemma orderOf_le_card_subgroup (hs : (s : Set α).Finite) (ha : a ∈ s) : orderOf a ≤ Nat.card s := by
   rw [← Nat.card_zpowers]; exact Nat.card_mono hs (zpowers_le.2 ha)
 
 end Group

LeanCamCombi/Mathlib/GroupTheory/MinOrder.lean

@@ -63,7 +63,7 @@ lemma le_minOrder' {n : ℕ∞} :
   · obtain ⟨a, has, ha⟩ := s.bot_or_exists_ne_one.resolve_left hs
     exact
       (h ha <| finite_zpowers.1 <| hs'.subset <| zpowers_le.2 has).trans
-        (WithTop.coe_le_coe.2 <| orderOf_le_card hs' has)
+        (WithTop.coe_le_coe.2 <| orderOf_le_card_subgroup hs' has)
   · simpa using h (zpowers_ne_bot.2 ha) ha'.finite_zpowers'
 
 @[to_additive]

LeanCamCombi/Mathlib/GroupTheory/OrderOfElement.lean

@@ -1,21 +1,71 @@
 import Mathlib.GroupTheory.OrderOfElement
+import LeanCamCombi.Mathlib.Data.Set.Finite
+import LeanCamCombi.Mathlib.SetTheory.Cardinal.Finite
 
---TODO: Turn `is_of_fin_order_iff_coe` around. Rename to `subgroup.is_of_fin_order_coe`
---TODO: Turn `is_of_fin_order_iff_coe` around. Rename to `subgroup.is_of_fin_order_coe`
+--TODO: Turn `isOfFinOrder_iff_coe` around. Rename to `Subgroup.isOfFinOrder_coe`
+--TODO: Turn `isOfFinOrder_iff_coe` around. Rename to `Subgroup.isOfFinOrder_coe`
 open Function Set Subgroup Submonoid
 
+variable {α : Type*}
+
 section Monoid
+variable [Monoid α] {a : α}
+
+-- TODO: Rename `orderOf_pos` to `orderOf_pos_of_finite`, or even delete it
+-- TODO: Replace `pow_eq_mod_orderOf`
+
+@[to_additive (attr := simp)]
+lemma pow_mod_orderOf (a : α) (n : ℕ) : a ^ (n % orderOf a) = a ^ n := pow_eq_mod_orderOf.symm
+
+@[to_additive] protected lemma IsOfFinOrder.orderOf_pos (ha : IsOfFinOrder a) : 0 < orderOf a :=
+  pos_iff_ne_zero.2 $ orderOf_eq_zero_iff.not_left.2 ha
+
+@[to_additive IsOfFinAddOrder.card_multiples_le_addOrderOf]
+lemma IsOfFinOrder.card_powers_le_orderOf (ha : IsOfFinOrder a) :
+    Nat.card (powers a : Set α) ≤ orderOf a := by
+  rw [←Fintype.card_fin (orderOf a), ←Nat.card_eq_fintype_card]
+  refine Nat.card_le_card_of_surjective (fun n ↦ ⟨a ^ (n : ℕ), by simp [mem_powers_iff]⟩) ?_
+  rintro ⟨b, n, rfl⟩
+  exact ⟨⟨n % orderOf a, Nat.mod_lt _ ha.orderOf_pos⟩, by simp⟩
+
+@[to_additive IsOfFinAddOrder.finite_multiples]
+lemma IsOfFinOrder.finite_powers (ha : IsOfFinOrder a) : (powers a : Set α).Finite := by
+  refine Set.Finite.of_surjOn (fun n ↦ a ^ n) ?_ (finite_Iio $ orderOf a)
+  rintro _ ⟨n, _, rfl⟩
+  exact ⟨n % orderOf a, Nat.mod_lt _ ha.orderOf_pos, by simp⟩
 
-variable {α : Type*} [Monoid α] {a : α}
-
--- --TODO: Fix name `order_eq_card_zpowers` to `order_of_eq_card_zpowers`
--- /-- See also `order_eq_card_powers`. -/
--- @[to_additive add_order_eq_card_multiples' "See also `add_order_eq_card_multiples`."]
--- lemma order_of_eq_card_powers' : order_of a = nat.card (powers a) := sorry
--- @[to_additive is_of_fin_add_order.finite_multiples]
--- lemma is_of_fin_order.finite_powers (h : is_of_fin_order a) : (powers a : set α).finite :=
--- begin
---   rw [←order_of_pos_iff, order_of_eq_card_powers'] at h,
---   exact finite_coe_iff.1 (nat.finite_of_card_ne_zero h.ne'),
--- end
 end Monoid
+
+section LeftCancelMonoid
+variable [LeftCancelMonoid α] {a : α}
+
+@[to_additive (attr := simp) finite_multiples]
+lemma finite_powers : (powers a : Set α).Finite ↔ IsOfFinOrder a := by
+  refine ⟨fun h ↦ ?_, IsOfFinOrder.finite_powers⟩
+  obtain ⟨m, n, hmn, ha⟩ := h.exists_lt_map_eq_of_forall_mem (f := fun n : ℕ ↦ a ^ n)
+    (fun n ↦ by simp [mem_powers_iff])
+  refine (isOfFinOrder_iff_pow_eq_one _).2 ⟨n - m, tsub_pos_iff_lt.2 hmn, ?_⟩
+  rw [←mul_left_cancel_iff (a := a ^ m), ←pow_add, add_tsub_cancel_of_le hmn.le, ha, mul_one]
+
+@[to_additive (attr := simp) infinite_multiples]
+lemma infinite_powers : (powers a : Set α).Infinite ↔ ¬ IsOfFinOrder a := finite_powers.not
+
+--TODO: Fix name `order_eq_card_zpowers` to `orderOf_eq_card_zpowers`
+--TODO: Rename ``
+/-- See also `orderOf_eq_card_powers`. -/
+@[to_additive Nat.card_addSubmonoidMultiples "See also `addOrder_eq_card_multiples`."]
+lemma Nat.card_submonoidPowers : Nat.card (powers a) = orderOf a := by
+  by_cases ha : IsOfFinOrder a
+  · symm
+    trans Nat.card (Fin (orderOf a))
+    · simp only [Nat.card_eq_fintype_card, Fintype.card_fin]
+    refine Nat.card_eq_of_bijective (fun n ↦ ⟨a ^ (n : ℕ), by simp [mem_powers_iff]⟩) ⟨?_, ?_⟩
+    · rintro m n hmn
+      simp [pow_eq_pow_iff_modEq] at hmn
+      exact Fin.ext $ hmn.eq_of_lt_of_lt m.2 n.2
+    · rintro ⟨b, n, rfl⟩
+      exact ⟨⟨n % orderOf a, Nat.mod_lt _ ha.orderOf_pos⟩, by simp⟩
+  · have := (infinite_powers.2 ha).to_subtype
+    rw [orderOf_eq_zero ha, Nat.card_eq_zero_of_infinite]
+
+end LeftCancelMonoid

LeanCamCombi/Mathlib/GroupTheory/Subgroup/Basic.lean

@@ -9,4 +9,7 @@ attribute [norm_cast] coe_eq_univ AddSubgroup.coe_eq_univ
 
 @[to_additive (attr := simp)] lemma coeSort_coe (s : Subgroup G) : ↥(s : Set G) = ↥s := rfl
 
+@[to_additive (attr := simp)]
+lemma nonempty (s : Subgroup G) : (s : Set G).Nonempty := ⟨1, one_mem _⟩
+
 end Subgroup

LeanCamCombi/Mathlib/SetTheory/Cardinal/Finite.lean

@@ -1,7 +1,25 @@
+import Mathlib.Control.ULift
 import Mathlib.SetTheory.Cardinal.Finite
 import LeanCamCombi.Mathlib.SetTheory.Cardinal.Basic
 
-open Cardinal
+open Cardinal Function
+
+universe u v u' v'
+
+namespace ULift
+variable {α : Type u} {β : Type v} {f : α → β}
+
+protected def map' (f : α → β) (a : ULift.{u'} α) : ULift.{v'} β := ULift.up.{v'} (f a.down)
+
+lemma map_injective (hf : Injective f) :
+    Injective (ULift.map' f : ULift.{u'} α → ULift.{v'} β) :=
+  up_injective.comp <| hf.comp down_injective
+
+lemma map_surjective (hf : Surjective f) :
+    Surjective (ULift.map' f : ULift.{u'} α → ULift.{v'} β) :=
+  up_surjective.comp <| hf.comp down_surjective
+
+end ULift
 
 namespace Nat
 variable {α : Type*}
@@ -17,6 +35,16 @@ lemma card_pos_iff : 0 < Nat.card α ↔ Nonempty α ∧ Finite α := by
 
 @[simp] lemma card_pos [Nonempty α] [Finite α] : 0 < Nat.card α := card_pos_iff.2 ⟨‹_›, ‹_›⟩
 
+lemma card_le_card_of_injective {α : Type u} {β : Type v} [Finite β] (f : α → β)
+    (hf : Injective f) : Nat.card α ≤ Nat.card β := by
+  simpa using toNat_le_of_le_of_lt_aleph0 (by simp [lt_aleph0_of_finite]) $
+    mk_le_of_injective (α := ULift.{max u v} α) (β := ULift.{max u v} β) $ ULift.map_injective hf
+
+lemma card_le_card_of_surjective {α : Type u} {β : Type v} [Finite α] (f : α → β)
+    (hf : Surjective f) : Nat.card β ≤ Nat.card α := by
+  simpa using toNat_le_of_le_of_lt_aleph0 (by simp [lt_aleph0_of_finite]) $
+    mk_le_of_surjective (α := ULift.{max u v} α) (β := ULift.{max u v} β) $ ULift.map_surjective hf
+
 -- TODO: Golf proof
 -- lemma finite_of_card_ne_zero (h : nat.card α ≠ 0) : finite α := (card_ne_zero.1 h).2
 lemma card_mono {s t : Set α} (ht : t.Finite) (h : s ⊆ t) : Nat.card s ≤ Nat.card t :=