max_power_factor — Mathlib

English

If a₀ ≠ 0 and x is non-unit in a commutative monoid with zero that satisfies WfDvdMonoid, there exists a power x^n and a residual a such that a₀ = x^n · a with a not divisible by x.

Русский

Если a₀ ≠ 0 и x не единица в коммутативном моноиде с нулём, удовлетворяющем WfDvdMonoid, то существует x^n и остаток a, чей делитель x не делит a, и a₀ = x^n a.

LaTeX

$$$\\exists n,a:\\mathbb{N}\\times α, \\ a_0 = x^n \\cdot a\\ \\wedge\\ \\lnot x \\mid a$$$

Lean4

theorem max_power_factor [CommMonoidWithZero α] [WfDvdMonoid α] {a₀ x : α} (h : a₀ ≠ 0) (hx : Irreducible x) :
    ∃ (n : ℕ) (a : α), ¬x ∣ a ∧ a₀ = x ^ n * a :=
  max_power_factor' h hx.not_isUnit

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