refl

Mathlib.RingTheory.Congruence.Defs

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

English

For every x, c x x.

Русский

Пусть c — конгруэнция на кольцо; для любого элемента x верно c x x.

LaTeX

$$$$\forall x,\ c x x.$$$$

Lean4

protected theorem refl (x) : c x x :=
  c.refl' x

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

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

Разделы

Аффилиация

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