instNontrivial — Mathlib

English

Let p be an odd prime and x,y ∈ ℕ with x > y, p ∣ x − y and p ∤ x. For Ne n ≠ 0 and even n, the p-adic valuation of x^n − y^n equals the valuation of x − y plus that of n: padicValNat p (x^n − y^n) = padicValNat p (x − y) + padicValNat p n.

Русский

Пусть p — нечётная простая, x>y, p|x−y и p∤x; для n≠0 чётного типа, v_p(x^n − y^n) = v_p(x−y) + v_p(n).

LaTeX

$$$\\forall x,y \\in \\mathbb{N},\\ p\\text{ нечётная простая},\\ x>y,\\ p \\mid (x-y),\\ p \\nmid x \\Rightarrow \\forall n \\neq 0,\\ 2|n \\Rightarrow \\mathrm{padicVal}_p(x^n - y^n) = \\mathrm{padicVal}_p(x - y) + \\mathrm{padicVal}_p(n)$$$

Lean4

instance [NumberField K] : Nontrivial (InfiniteAdeleRing K) :=
  (inferInstanceAs <| Nonempty (InfinitePlace K)).elim fun w => Pi.nontrivial_at w

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