of_b_eq_zero — Mathlib

English

Let P be a cubic with coefficients a, b, c, d in a semiring R. If a = 0 and b = 0, then the polynomial associated to P is the linear polynomial with coefficients c and d, i.e. P.toPoly = C(P.c) · X + C(P.d).

Русский

Пусть P — кубический полином над полем/кольцом R с коэффициентами a, b, c, d. Если a = 0 и b = 0, то соответствующий полином P.toPoly имеет вид линейного полинома: P.toPoly = C(P.c) · X + C(P.d).

LaTeX

$$$ P.a = 0 \\land P.b = 0 \\Rightarrow P.toPoly = C(P.c) \\cdot X + C(P.d) $$$

Lean4

theorem of_b_eq_zero (ha : P.a = 0) (hb : P.b = 0) : P.toPoly = C P.c * X + C P.d := by
  rw [of_a_eq_zero ha, hb, C_0, zero_mul, zero_add]

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