range_isScalarTower_toAlgHom — Mathlib

English

The range of the IsScalarTower-toAlgHom map coincides with the submodule underlying S, i.e., the image is exactly the same as the submodule of S.

Русский

Образ IsScalarTower-toAlgHom совпадает с подмодулем, лежащим в S.

LaTeX

$$Range(IsScalarTower.toAlgHom R S A) = Subalgebra.toSubmodule S$$

Lean4

@[simp]
theorem range_isScalarTower_toAlgHom [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) :
    LinearMap.range (IsScalarTower.toAlgHom R S A) = Subalgebra.toSubmodule S :=
  by
  ext
  simp [algebraMap_eq]

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