map_toNonUnitalSubsemiring — Mathlib

English

The underlying nonunital subsemiring of the mapped subalgebra equals the image of the mapped subsemiring under the corresponding ring homomorphism.

Русский

Область подп-semiring отображения совпадает с образом соответствующего гомоморфизма кольца.

LaTeX

$$$ (\\mathrm{map}\, f\\ S)^{\\mathrm{toNonUnitalSubsemiring}} = S^{\\mathrm{toNonUnitalSubsemiring}}.map (f : A \\to_{n+}^* B). $$$

Lean4

theorem map_toNonUnitalSubsemiring {S : NonUnitalSubalgebra R A} {f : F} :
    (map f S).toNonUnitalSubsemiring = S.toNonUnitalSubsemiring.map (f : A →ₙ+* B) :=
  SetLike.coe_injective rfl

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