mk_eq_zero

Mathlib.Algebra.Module.Submodule.Defs

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

English

In the submodule, the equivalence class of an element with respect to zero reflects its zero-ness.

Русский

В подмодуле эквивалентность элемента относительно нуля отражает его нулевость.

LaTeX

$$$ (x,h) : (\\langle x,h\\rangle : p) = 0 \\iff x = 0 $$$

Lean4

@[simp]
theorem mk_eq_zero {x} (h : x ∈ p) : (⟨x, h⟩ : p) = 0 ↔ x = 0 :=
  Subtype.ext_iff

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

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

Разделы

Аффилиация

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