instTrans — Mathlib

English

There is a transitive structure for ModEq: if a ≡ b (mod n) and b ≡ c (mod n), then a ≡ c (mod n).

Русский

Свойство транзитивности для модульного эквивалентного отношения: если a ≡ b (mod n) и b ≡ c (mod n), то a ≡ c (mod n).

LaTeX

$$$a \\equiv b \\pmod{n} \\Rightarrow b \\equiv c \\pmod{n} \\Rightarrow a \\equiv c \\pmod{n}$$$

Lean4

instance : Trans (ModEq n) (ModEq n) (ModEq n) where trans := Nat.ModEq.trans

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