comm

Mathlib.LinearAlgebra.SModEq

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

English

Equivalence modulo U is symmetric: (x ≡ y) iff (y ≡ x).

Русский

Эквивалентность по модулю U симметрична: (x ≡ y) тогда и только тогда, когда (y ≡ x).

LaTeX

$$$ x \\equiv y [SMOD U] \\iff y \\equiv x [SMOD U]$$$

Lean4

theorem comm : x ≡ y [SMOD U] ↔ y ≡ x [SMOD U] :=
  ⟨symm, symm⟩

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

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

Разделы

Аффилиация

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