trans — Mathlib

English

If H is commensurable with K and K is commensurable with L, then H is commensurable with L.

Русский

Если H комменсурируемо относительно K, а K комменсурируемо относительно L, то H комменсурируемо относительно L.

LaTeX

$$Commensurable H K → Commensurable K L → Commensurable H L$$

Lean4

@[to_additive (attr := trans)]
theorem trans {H K L : Subgroup G} (hhk : Commensurable H K) (hkl : Commensurable K L) : Commensurable H L :=
  ⟨Subgroup.relIndex_ne_zero_trans hhk.1 hkl.1, Subgroup.relIndex_ne_zero_trans hkl.2 hhk.2⟩

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