factorization_ordCompl — Mathlib

English

(ordCompl_p(n)).factorization = n.factorization.erase p.

Русский

Факторизация ordCompl_p(n) равна факторизации n с удалением p.

LaTeX

$$$$ (\operatorname{ordCompl}_{p}(n)).\text{factorization} = n.\text{factorization}.erase(p). $$$$

Lean4

theorem factorization_ordCompl (n p : ℕ) : (ordCompl[p] n).factorization = n.factorization.erase p := by
  if hn : n = 0 then simp [hn]
  else
    if pp : p.Prime then ?_ else simp [pp]
    ext q
    rcases eq_or_ne q p with (rfl | hqp)
    · simp only [Finsupp.erase_same, factorization_eq_zero_iff, not_dvd_ordCompl pp hn]
      simp
    · rw [Finsupp.erase_ne hqp, factorization_div (ordProj_dvd n p)]
      simp [pp.factorization, hqp.symm]
        -- `ordCompl[p] n` is the largest divisor of `n` not divisible by `p`.

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