mul — Mathlib

English

If f and g are monic with respect to m, then their product is monic (assuming a nontrivial ring).

Русский

Если f и g моноидны относительно m, то их произведение моноидно (при условииом кольца не нулевое).

LaTeX

$$$$ m.Monic(f) \land m.Monic(g) \implies m.Monic(fg). $$$$

Lean4

theorem mul {f g : MvPolynomial σ R} (hf : m.Monic f) (hg : m.Monic g) : m.Monic (f * g) :=
  by
  nontriviality R
  suffices m.leadingCoeff f * m.leadingCoeff g = 1
    by
    rw [Monic, MonomialOrder.leadingCoeff, degree_mul_of_mul_leadingCoeff_ne_zero, coeff_mul_of_degree_add, this]
    rw [this]
    exact one_ne_zero
  rw [hf.leadingCoeff_eq_one, hg.leadingCoeff_eq_one, one_mul]

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