bot_ext

Mathlib.Algebra.Module.Submodule.Lattice

URI: https://scilib.ai/kg/mathlib#Submodule.bot_ext

English

Two bottom elements (in Submodule) are equal; the bottom submodule is a singleton.

Русский

Два нижних элемента (в Submodule) равны; нижний подмодуль является синглтоном.

LaTeX

$$x = y for x,y ∈ ⊥$$

Lean4

@[ext high]
protected theorem bot_ext (x y : (⊥ : Submodule R M)) : x = y := by subsingleton

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

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

Разделы

Аффилиация

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