leadingCoeff_mul — Mathlib

English

If R is a semiring with no zero divisors, then the leading coefficient is multiplicative: lc(p q) = lc(p) lc(q) for all p, q ∈ R[X].

Русский

Пусть R — полугруппа без нулевых делителей; ведущий коэффициент умножения сохраняется: lc(p q) = lc(p) lc(q) для любых p, q ∈ R[X].

LaTeX

$$$\operatorname{lc}(p q)=\operatorname{lc}(p)\operatorname{lc}(q).$$$

Lean4

@[simp]
theorem leadingCoeff_mul (p q : R[X]) : leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q :=
  by
  by_cases hp : p = 0
  · simp only [hp, zero_mul, leadingCoeff_zero]
  · by_cases hq : q = 0
    · simp only [hq, mul_zero, leadingCoeff_zero]
    · rw [leadingCoeff_mul']
      exact mul_ne_zero (mt leadingCoeff_eq_zero.1 hp) (mt leadingCoeff_eq_zero.1 hq)

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