relIndex_mul_index — Mathlib

English

A relation linking relIndex of an intersection with a product of relIndices for subgroups.

Русский

Связь relIndex пересечения с произведением relIndex подгрупп.

LaTeX

$$$\\mathrm{relIndex}(H, K \\cap L) \\cdot \\mathrm{relIndex}(K, L) = \\mathrm{relIndex}(H \\cap K, L).$$$

Lean4

@[to_additive relIndex_mul_index]
theorem relIndex_mul_index (h : H ≤ K) : H.relIndex K * K.index = H.index :=
  ((mul_comm _ _).trans (Cardinal.toNat_mul _ _).symm).trans
    (congr_arg Cardinal.toNat (Equiv.cardinal_eq (quotientEquivProdOfLE h))).symm

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