Nontrivial divisible group is infinite

Stream: Is there code for X?

[Stepan Nesterov]

Is the following lemma a special case of something already in Mathlib?

lemma infinite_of_divisible_nontrivial (A : Type*) [AddGroup A] [DivisibleBy A ℕ] [Nontrivial A] :
    Infinite A := by
  obtain ⟨a, a_nz⟩ := exists_ne (0 : A)
  by_cases ha : IsOfFinAddOrder a
  . rw [isOfFinAddOrder_iff_nsmul_eq_zero] at ha
    obtain ⟨n, n_pos, hn⟩ := ha
    let f : ℕ → A := Nat.rec (motive := fun _ => A) a (fun _ fk => DivisibleBy.div fk n)
    have f_zero : f 0 = a := rfl
    have f_succ : ∀ k : ℕ, f k.succ = DivisibleBy.div (f k) n := by intro k; rfl
    have hf : ∀ k l : ℕ, n ^ l • f (k + l) = f k := by
      intro k l
      induction l generalizing k with
        | zero => simp
        | succ l hl =>
          rw [pow_add, mul_nsmul, add_comm l 1, ← add_assoc, hl (k + 1), pow_one]
          dsimp [f]
          rw [DivisibleBy.div_cancel]
          exact Nat.ne_zero_of_lt n_pos
    have hf' : ∀ l : ℕ, n ^ l • f l = a := by
      intro l
      nth_rewrite 2 [← zero_add l]
      rw [hf]
      rfl
    apply Infinite.of_injective f
    intro k k' hkk'
    by_contra k_ne_k'
    change k ≠ k' at k_ne_k'
    wlog h : k < k' generalizing k k'
    · symm at hkk' k_ne_k'
      specialize this hkk' k_ne_k'
      apply this
      obtain h' | h' | h' := lt_trichotomy k k'
      · contradiction
      · symm at h'
        contradiction
      · exact h'
    · rw [lt_iff_exists_pos_add] at h
      obtain ⟨l, l_pos, hl⟩ := h
      rw [← hl] at hkk'
      apply_fun (fun (a : A) => n ^ k • a) at hkk'
      rw [add_comm, hf, hf'] at hkk'
      rw [← Nat.succ_pred_eq_of_pos l_pos, f_succ] at hkk'
      apply_fun (fun (a : A) => n • a) at hkk'
      rw [hn, DivisibleBy.div_cancel _ (Nat.ne_zero_of_lt n_pos)] at hkk'
      apply_fun (fun (a : A) => n ^ (l.pred) • a) at hkk'
      rw [hf', nsmul_zero] at hkk'
      symm at hkk'
      contradiction
  · rw [← injective_nsmul_iff_not_isOfFinAddOrder] at ha
    exact Infinite.of_injective _ ha

If not, is it worth trying to PR it into file#Mathlib/GroupTheory/Divisible ?

[Damiano Testa]

I wonder if it would be easier to formalise that a nontrivial element of a finite group cannot be divisible by the order of the group.

[Damiano Testa]

So, something like this:

lemma infinite_of_divisible_nontrivial (A : Type*) [AddGroup A] [DivisibleBy A ℕ] [Nontrivial A] :
    Infinite A := by
  obtain ⟨a, a_nz⟩ := exists_ne (0 : A)
  contrapose! a_nz with A_finite
  let : Fintype A := Fintype.ofFinite A
  have := DivisibleBy.div_cancel (n := Fintype.card A) a (by simp)
  simp_all