monic_expand_iff — Mathlib

English

For p > 0, Eq (AlgHom.coef (expand R p) f).leadingCoeff = f.leadingCoeff.

Русский

Для p > 0, ведущий коэффициент $AlgHom.coef(expand R p) f$ равен ведущему коэффициенту f.

LaTeX

$$$\text{leadingCoeff}(\mathrm{expand}\ R\ p\ f) = \text{leadingCoeff}(f)$ under $0 < p$$$

Lean4

theorem monic_expand_iff {p : ℕ} {f : R[X]} (hp : 0 < p) : (expand R p f).Monic ↔ f.Monic := by
  simp only [Monic, leadingCoeff_expand hp]

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