relIndex_mul_relIndex — Mathlib

English

If H ≤ K ≤ L, then H.relIndex K · K.relIndex L = H.relIndex L.

Русский

Если H ≤ K ≤ L, то H.relIndex K умножить на K.relIndex L равно H.relIndex L.

LaTeX

$$$H.relIndex K \\cdot K.relIndex L = H.relIndex L$ при $H \\le K \\le L$.$$

Lean4

@[to_additive relIndex_mul_relIndex]
theorem relIndex_mul_relIndex (hHK : H ≤ K) (hKL : K ≤ L) : H.relIndex K * K.relIndex L = H.relIndex L :=
  by
  rw [← relIndex_subgroupOf hKL]
  exact relIndex_mul_index fun x hx => hHK hx

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