irrational_sqrt_of_multiplicity_odd

English

Let m ∈ ℤ, m > 0, p prime, and the p-adic multiplicity of m is odd. Then sqrt(m) is irrational.

Русский

Пусть m ∈ ℤ, m > 0, p — простое, и p-адическая кратность m нечётна. Тогда sqrt(m) иррационально.

LaTeX

$$$\forall m \in \mathbb{Z}, m > 0, \exists p\text{ prime}, \operatorname{multiplicity}(p, m) \\% 2 = 1 \Rightarrow \mathrm{Irrational}(\sqrt{m})$$$

Lean4

theorem irrational_sqrt_of_multiplicity_odd (m : ℤ) (hm : 0 < m) (p : ℕ) [hp : Fact p.Prime]
    (Hpv : multiplicity (p : ℤ) m % 2 = 1) : Irrational (√m) :=
  @irrational_nrt_of_n_not_dvd_multiplicity _ 2 _ (Ne.symm (ne_of_lt hm)) p hp
    (sq_sqrt (Int.cast_nonneg.2 <| le_of_lt hm)) (by rw [Hpv]; exact one_ne_zero)

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