C — Mathlib · SciLib

English

The constant embedding C: R → LaurentPolynomial R is defined as the constant Laurent polynomials.

Русский

Константное вложение C: R → LaurentPolynomial R задаёт константные лорантовые полиномы.

LaTeX

$$$\\mathsf{C}: R \\to^+ R[T;T^{-1}]$ is the constant Laurent polynomial embedding.$$

Lean4

/-- The ring homomorphism `C`, including `R` into the ring of Laurent polynomials over `R` as
the constant Laurent polynomials. -/
def C : R →+* R[T;T⁻¹] :=
  singleZeroRingHom

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