divisibleByIntOfSMulTopEqTop — Mathlib

English

If for all n ≠ 0 in ℤ we have n • ⊤ = ⊤, then A is divisible by ℤ.

Русский

Если для всех n ≠ 0 ∈ ℤ выполняется n • ⊤ = ⊤, то A делимо по ℤ.

LaTeX

$$$\Big(\forall {n : \mathbb{Z}}, n \neq 0 \rightarrow n \cdot \top = \top\Big) \Rightarrow \text{DivisibleBy } A \mathbb{Z}$$$

Lean4

/-- If for all `n ≠ 0 ∈ ℤ`, `n • A = A`, then `A` is divisible.
-/
noncomputable def divisibleByIntOfSMulTopEqTop (H : ∀ {n : ℤ} (_hn : n ≠ 0), n • (⊤ : AddSubgroup A) = ⊤) :
    DivisibleBy A ℤ
    where
  div a n := if hn : n = 0 then 0 else (show a ∈ n • (⊤ : AddSubgroup A) by rw [H hn]; trivial).choose
  div_zero _ := dif_pos rfl
  div_cancel a
    hn := by
    simp_rw [dif_neg hn]
    generalize_proofs h1
    exact h1.choose_spec.2

Похожие утверждения