refl

Mathlib.LinearAlgebra.SModEq

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

English

Reflexivity: every element is equivalent to itself modulo U.

Русский

Рефлексивность: каждый элемент эквивалентен сам себе по модулю U.

LaTeX

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

Lean4

@[refl]
protected theorem refl (x : M) : x ≡ x [SMOD U] :=
  @rfl _ _

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

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

Разделы

Аффилиация

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