relIndex_le_of_le_right — Mathlib

English

If K ≤ L and H.relIndex L ≠ 0, then H.relIndex K ≤ H.relIndex L.

Русский

Если K ⊆ L и H.relIndex L ≠ 0, то H.relIndex K ≤ H.relIndex L.

LaTeX

$$$(hKL : K \le L) \rightarrow (hHL : H.\relIndex L \neq 0) \rightarrow H.\relIndex K ≤ H.\relIndex L$$$

Lean4

@[to_additive]
theorem relIndex_le_of_le_right (hKL : K ≤ L) (hHL : H.relIndex L ≠ 0) : H.relIndex K ≤ H.relIndex L :=
  Finite.card_le_of_embedding' (quotientSubgroupOfEmbeddingOfLE H hKL) fun h => (hHL h).elim

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