mem_algebraMapSubmonoid_of_mem

Mathlib.Algebra.Algebra.Basic

URI: https://scilib.ai/kg/mathlib#Algebra.mem_algebraMapSubmonoid_of_mem

← MathLib Explorer

English

If x ∈ M, then algebraMap R S x ∈ algebraMapSubmonoid S M (same as above).

Русский

Если x ∈ M, то algebraMap R S x ∈ algebraMapSubmonoid S M (то же самое).

LaTeX

$$algebraMap R S x ∈ algebraMapSubmonoid S M$$

Lean4

theorem mem_algebraMapSubmonoid_of_mem {S : Type*} [Semiring S] [Algebra R S] {M : Submonoid R} (x : M) :
    algebraMap R S x ∈ algebraMapSubmonoid S M :=
  Set.mem_image_of_mem (algebraMap R S) x.2

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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