monomial_natDegree_leadingCoeff_eq_self

English

If the support of p has at most one element, then p equals the monomial with exponent natDegree(p) and coefficient leadingCoeff(p).

Русский

Если поддержка p содержит не более одного элемента, то p равен мономию $X^{\\operatorname{natDegree}(p)}$ с коэффициентом $\\operatorname{leadingCoeff}(p)$.

LaTeX

$$$\\#p.\\operatorname{support} \\le 1 \\Rightarrow \\operatorname{monomial}(\\operatorname{natDegree}(p), \\operatorname{leadingCoeff}(p)) = p$$$

Lean4

theorem monomial_natDegree_leadingCoeff_eq_self (h : #p.support ≤ 1) : monomial p.natDegree p.leadingCoeff = p := by
  classical
  rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩
  by_cases ha : a = 0 <;> simp [ha]

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