C — Mathlib · SciLib

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 }

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