trans

Mathlib.RingTheory.Congruence.Defs

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

English

If c x y and c y z, then c x z.

Русский

Если x конгруэнтен y, а y конгруэнтен z, то x конгруэнтен z.

LaTeX

$$$$\forall x y z,\ c x y \Rightarrow c y z \Rightarrow c x z.$$$$

Lean4

protected theorem trans {x y z} : c x y → c y z → c x z :=
  c.trans'

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

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

Разделы

Аффилиация

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