instIsTransModEq

Mathlib.Algebra.ModEq

URI: https://scilib.ai/kg/mathlib#AddCommGroup.instIsTransModEq

English

The relation of congruence modulo p is transitive.

Русский

Отношение конгруэнтности по модулю p транзитивно.

LaTeX

$$$\forall a,b,c,\ a \equiv b [PMOD p] \land b \equiv c [PMOD p] \Rightarrow a \equiv c [PMOD p]$$$

Lean4

instance : IsTrans α (ModEq p) where trans _ _ _ := ModEq.trans

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

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

Разделы

Аффилиация

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