coeRingHom_of — Mathlib

English

There is a canonical ring homomorphism from the direct sum to R witnessing the ring structure, reflecting the graded components.

Русский

Существует каноническое кольцо-гомоморфизм от прямой суммы к R, фиксирующий кольцевую структуру.

LaTeX

$$DirectSum.coeRingHom : (⨁ i, A i) →+* R$$

Lean4

/-- The canonical ring isomorphism between `⨁ i, A i` and `R` -/
@[simp]
theorem coeRingHom_of [AddMonoid ι] [SetLike.GradedMonoid A] (i : ι) (x : A i) :
    (coeRingHom A : _ →+* R) (of (fun i => A i) i x) = x :=
  DirectSum.toSemiring_of _ _ _ _ _

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