decomposeRingEquiv — Mathlib

English

A graded ring A by ι is canonically isomorphic to the direct sum of its graded components ⨁ i 𝒜 i.

Русский

Градуированное кольцо A по ι канонически изоморфно прямой сумме его компонент 𝒜 i.

LaTeX

$$$ A \cong \bigoplus_{i\in \iota} 𝒜(i). $$$

Lean4

/-- If `A` is graded by `ι` with degree `i` component `𝒜 i`, then it is isomorphic as
a ring to a direct sum of components. -/
def decomposeRingEquiv : A ≃+* ⨁ i, 𝒜 i :=
  RingEquiv.symm { (decomposeAddEquiv 𝒜).symm with map_mul' := (coeRingHom 𝒜).map_mul }

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