symm

Mathlib.LinearAlgebra.SModEq

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

English

Symmetry: if x is equivalent to y modulo U, then y is equivalent to x modulo U.

Русский

Симметрия: если x эквивалентен y по модулю U, то y эквивалентен x по модулю U.

LaTeX

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

Lean4

@[symm]
nonrec theorem symm (hxy : x ≡ y [SMOD U]) : y ≡ x [SMOD U] :=
  hxy.symm

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

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

Разделы

Аффилиация

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