ordCompl_mul — Mathlib

English

For all natural numbers a, b and p, the p-order complement is multiplicative over multiplication: ordCompl_p(ab) = ordCompl_p(a) ordCompl_p(b).

Русский

Для любых натуральных чисел a, b и p выполнено: ordCompl_p(ab) = ordCompl_p(a) ordCompl_p(b).

LaTeX

$$$$\operatorname{ordCompl}_{p}(ab) = \operatorname{ordCompl}_{p}(a)\,\operatorname{ordCompl}_{p}(b).$$$$

Lean4

theorem ordCompl_mul (a b p : ℕ) : ordCompl[p] (a * b) = ordCompl[p] a * ordCompl[p] b := by
  if ha : a = 0 then simp [ha]
  else
    if hb : b = 0 then simp [hb]
    else
      simp only [ordProj_mul p ha hb]
      rw [div_mul_div_comm (ordProj_dvd a p) (ordProj_dvd b p)]

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