constantCoeff_comp_C — Mathlib

English

The constant-coefficient map after embedding scalars via C is the identity on the base ring: constantCoeff ∘ C = id.

Русский

Пусть константный коэффициент после внедрения скаляров через C совпадает с тождеством на основании кольца: constantCoeff ∘ C = id.

LaTeX

$$$\\forall R\\ [\\operatorname{Semiring} R],\\ constantCoeff \\circ C = \\mathrm{id}_R$$$

Lean4

@[simp]
theorem constantCoeff_comp_C : constantCoeff.comp C = RingHom.id R :=
  rfl

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