mk_eq_zero

Mathlib.LinearAlgebra.Quotient.Defs

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

English

The coset [x] is zero iff x ∈ p.

Русский

Косет [x] равен нулю тогда, когда x ∈ p.

LaTeX

$$$(\operatorname{mk} x) = 0 \iff x \in p$$$

Lean4

@[simp]
theorem mk_eq_zero : (mk x : M ⧸ p) = 0 ↔ x ∈ p := by simpa using (Quotient.eq' p : mk x = 0 ↔ _)

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

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

Разделы

Аффилиация

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