instIsTransDvd

Mathlib.Algebra.Divisibility.Basic

URI: https://scilib.ai/kg/mathlib#instIsTransDvd

English

Divisibility is a transitive relation.

Русский

Делимость — транзитивное отношение.

LaTeX

$$$$\text{IsTrans }(\cdot \mid \cdot)$$$$

Lean4

/-- Transitivity of `|` for use in `calc` blocks. -/
instance : IsTrans α Dvd.dvd :=
  ⟨fun _ _ _ => dvd_trans⟩

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

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

Разделы

Аффилиация

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