English
There is a natural equivalence between cubic polynomials and polynomials of degree at most three over R; the equivalence is given by mapping a cubic to its associated degree-≤3 polynomial and by extracting coefficients.
Русский
Существует биекция между кубическими многочленами над кольцом R и многочленами степени не выше тройки над R; соответствие задаётся отображением кубического полинома к соответствующему многочлену в R[X] с степенью ≤ 3 и обратным извлечением коэффициентов.
LaTeX
$$$\\Cubic(R) \\cong { p \\in R[X] \\mid \\deg(p) \\le 3 }$$$
Lean4
/-- The equivalence between cubic polynomials and polynomials of degree at most three. -/
@[simps]
def equiv : Cubic R ≃ { p : R[X] // p.degree ≤ 3 }
where
toFun P := ⟨P.toPoly, degree_cubic_le⟩
invFun f := ⟨coeff f 3, coeff f 2, coeff f 1, coeff f 0⟩
left_inv P := by ext <;> simp only [coeffs]
right_inv
f := by
ext n
obtain hn | hn := le_or_gt n 3
· interval_cases n <;> simp only <;> ring_nf <;> try simp only [coeffs]
· rw [coeff_eq_zero hn, (degree_le_iff_coeff_zero (f : R[X]) 3).mp f.2]
simpa using hn
