instIsTrans

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Associated.instIsTrans

English

There is an IsTrans instance for Associated on any monoid.

Русский

Для Associated на любом моноиде существует инстанс IsTrans.

LaTeX

$$$\\forall x,y,z\\, Associated x y \\wedge Associated y z \\Rightarrow Associated x z$$$

Lean4

instance [Monoid M] : IsTrans M Associated :=
  ⟨fun _ _ _ => Associated.trans⟩

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

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

Разделы

Аффилиация

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