coe_bot

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalAlgebra.coe_bot

English

The underlying set of the bottom subalgebra equals {0}.

Русский

Основание нижней подпалгебры совпадает с множеством {0}.

LaTeX

$$$ (\\bot : \\mathrm{NonUnitalSubalgebra}\\, R\\, A) \\; = \\; \\{0\\} $$$

Lean4

@[simp, norm_cast]
theorem coe_bot : ((⊥ : NonUnitalSubalgebra R A) : Set A) = {0} := by simp [Set.ext_iff, NonUnitalAlgebra.mem_bot]

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

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

Разделы

Аффилиация

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