uniqueBot

Mathlib.Algebra.Module.Submodule.Lattice

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

English

A submodule p equals the bottom iff every element of p is zero.

Русский

Подмодуль p равен нижнему эквивалентно тому, что каждый элемент p равен нулю.

LaTeX

$$$p = \bot \iff \forall x \in p,\ x = 0$$$

Lean4

instance uniqueBot : Unique (⊥ : Submodule R M) :=
  ⟨inferInstance, fun x ↦ Subtype.ext <| (mem_bot R).1 x.mem⟩

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

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

Разделы

Аффилиация

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