max_power_factor' — Mathlib

English

Reiterates that there exists a NormalizedGCDMonoid structure on a UniqueFactorizationMonoid.

Русский

Повторение существования структуры NormalizedGCDMonoid на UniqueFactorizationMonoid.

LaTeX

$$$\\exists\\; N : NormalizedGCDMonoid\\ α$$$

Lean4

theorem max_power_factor' [CommMonoidWithZero α] [WfDvdMonoid α] {a₀ x : α} (h : a₀ ≠ 0) (hx : ¬IsUnit x) :
    ∃ (n : ℕ) (a : α), ¬x ∣ a ∧ a₀ = x ^ n * a :=
  by
  obtain ⟨a, ⟨n, rfl⟩, hm⟩ :=
    wellFounded_dvdNotUnit.has_min {a | ∃ n, x ^ n * a = a₀} ⟨a₀, 0, by rw [pow_zero, one_mul]⟩
  refine ⟨n, a, ?_, rfl⟩; rintro ⟨d, rfl⟩
  exact
    hm d ⟨n + 1, by rw [pow_succ, mul_assoc]⟩ ⟨(right_ne_zero_of_mul <| right_ne_zero_of_mul h), x, hx, mul_comm _ _⟩

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