of_not_isUnit — Mathlib

English

In a commutative monoid with zero and WfDvdMonoid, for a nonzero a and irreducible x, there exists n and a such that a = x^n · a with a not divisible by x.

Русский

В коммутативном моноиде с нулём и WfDvdMonoid для ненулевого a и ирредуцируемого x существуют n и a такие, что a = x^n · a и a не делится на x.

LaTeX

$$$\\text{max_power_factor}(a_0,x)\\;:\\; \\exists n, a:\\mathbb{N} \\times α, \\ a_0 = x^n \\cdot a \\land \\lnot x \\mid a$$$

Lean4

theorem of_not_isUnit [CancelCommMonoidWithZero α] [WfDvdMonoid α] {a b : α} (ha : ¬IsUnit a) (hb : b ≠ 0) :
    FiniteMultiplicity a b :=
  by
  obtain ⟨n, c, ndvd, rfl⟩ := WfDvdMonoid.max_power_factor' hb ha
  exact ⟨n, by rwa [pow_succ, mul_dvd_mul_iff_left (left_ne_zero_of_mul hb)]⟩

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