rangeS_le

Mathlib.Algebra.Algebra.Subalgebra.Basic

URI: https://scilib.ai/kg/mathlib#Subalgebra.rangeS_le

English

The range of the algebra map from R to A is contained in the underlying subsemiring of any subalgebra S.

Русский

Образ отображения алгебраMap(R,A) в A лежит в подповерхности S.

LaTeX

$$$ (\mathrm{algebraMap}\; R\; A).\mathrm{rangeS} \le S.toSubsemiring $$$

Lean4

theorem rangeS_le : (algebraMap R A).rangeS ≤ S.toSubsemiring := fun _x ⟨r, hr⟩ => hr ▸ S.algebraMap_mem r

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru