rangeS_algebraMap — Mathlib

English

The range of the map algebraMap from S to A equals the underlying Subsemiring of S.

Русский

Образ отображения algebraMap с S в A равен подполуподкольцу S (подполу-семирину).

LaTeX

$$$\operatorname{range}(\mathrm{algebraMap}_{S}^{A}) = S^{\text{toSubsemiring}}$$$

Lean4

@[simp]
theorem rangeS_algebraMap {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) :
    (algebraMap S A).rangeS = S.toSubsemiring := by
  rw [algebraMap_eq, Algebra.algebraMap_self, RingHom.id_comp, ← toSubsemiring_subtype, Subsemiring.rangeS_subtype]

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