algebraMap_apply — Mathlib

English

The algebra map algebraMap R (LaurentPolynomial A) r equals the constant Laurent term C(algebraMap R A r).

Русский

Алгебраическое отображение algebraMap R (LaurentPolynomial A) r равно константному лорантовому члену C(algebraMap R A r).

LaTeX

$$$\\operatorname{algebraMap}_{R, \\LaurentPolynomial A}(r) = C\\bigl(\\operatorname{algebraMap}_{R A}(r)\\bigr)$$$

Lean4

theorem algebraMap_apply {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) :
    algebraMap R (LaurentPolynomial A) r = C (algebraMap R A r) :=
  rfl

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