subset_coe_one

Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

URI: https://scilib.ai/kg/mathlib#SubMulAction.subset_coe_one

English

The singleton one set is contained in the carrier of the SubMulAction one.

Русский

Единственный элемент множества единицы содержится в носителе единицы SubMulAction.

LaTeX

$$$ (1 : \\mathrm{Set} M) \\subseteq (1 : \\mathrm{SubMulAction} \\; R \\; M). $$$

Lean4

theorem subset_coe_one : (1 : Set M) ⊆ (1 : SubMulAction R M) := fun _ hx => ⟨1, (one_smul _ _).trans hx.symm⟩

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

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

Разделы

Аффилиация

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