degree_smul_of_isRightRegular_leadingCoeff

English

If a ≠ 0 and p.leadingCoeff is right-regular, then deg(a • p) = deg(p).

Русский

Если a ≠ 0 и p.leadingCoeff является правым регулярным, то deg(a • p) = deg(p).

LaTeX

$$$ (a \cdot p).degree = p.degree \quad\text{if } a \neq 0 \text{ and } IsRightRegular(p.leadingCoeff). $$$

Lean4

theorem degree_smul_of_isRightRegular_leadingCoeff (ha : a ≠ 0) (hp : IsRightRegular p.leadingCoeff) :
    (a • p).degree = p.degree :=
  by
  refine le_antisymm (degree_smul_le a p) <| degree_le_degree ?_
  rw [coeff_smul, coeff_natDegree, smul_eq_mul, ne_eq]
  exact hp.mul_right_eq_zero_iff.ne.mpr ha

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