English
C a is the constant polynomial with value a; C is a ring homomorphism.
Русский
C a — константный полином со значением a; C — гомоморфизм колец.
LaTeX
$$$\mathrm{C}(a) : = \text{constant polynomial with value } a$$$
Lean4
/-- `C a` is the constant polynomial `a`.
`C` is provided as a ring homomorphism.
-/
def C : R →+* R[X] :=
{ monomial 0 with
map_one' := by simp [monomial_zero_one]
map_mul' := by simp [monomial_mul_monomial]
map_zero' := by simp }