natDegree_of_b_ne_zero — Mathlib

English

Let P be a cubic polynomial with coefficients a, b, c, d. If a = 0 and b ≠ 0, then the natural degree of the associated polynomial P.toPoly is 2.

Русский

Пусть P является кубическим полиномом с коэффициентами a, b, c, d. Если a = 0 и b ≠ 0, то естественная степень связанного полинома P.toPoly равна 2.

LaTeX

$$$$P.a = 0 \land P.b \\ne 0 \\implies \\operatorname{natDegree}(P.toPoly) = 2.$$$$

Lean4

@[simp]
theorem natDegree_of_b_ne_zero (ha : P.a = 0) (hb : P.b ≠ 0) : P.toPoly.natDegree = 2 := by
  rw [of_a_eq_zero ha, natDegree_quadratic hb]

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