coe_eq_zero

Mathlib.Algebra.Module.Submodule.Defs

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

English

Equality of the coercion to the ambient module with zero corresponds to zero in the submodule.

Русский

Равенство приводимого элемента к нулю в модуле-окружении соответствует нулю в подмодуле.

LaTeX

$$$ {x} : p \\Rightarrow ((x : M) = 0) \\iff x = 0 $$$

Lean4

@[norm_cast]
theorem coe_eq_zero {x : p} : (x : M) = 0 ↔ x = 0 :=
  (SetLike.coe_eq_coe : (x : M) = (0 : p) ↔ x = 0)

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

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

Разделы

Аффилиация

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