zero

Mathlib.LinearAlgebra.SModEq

URI: https://scilib.ai/kg/mathlib#SModEq.zero

English

x ≡ 0 mod U iff x ∈ U.

Русский

x ≡ 0 mod U тогда и только тогда, когда x ∈ U.

LaTeX

$$$$ x \\equiv 0\\ [SMOD\\ U] \\iff x \\in U. $$$$

Lean4

theorem zero : x ≡ 0 [SMOD U] ↔ x ∈ U := by rw [SModEq.def, Submodule.Quotient.eq, sub_zero]

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

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

Разделы

Аффилиация

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