card_right — Mathlib

English

If IsComplement S H holds, then card of T equals the index of H: Nat.card T.Elem = H.index.

Русский

Если S является дополнением H, то Nat.card T.Elem = H.index.

LaTeX

$$Nat.card T.Elem = H.index$$

Lean4

@[to_additive]
theorem card_right (h : IsComplement H T) : Nat.card T = H.index :=
  Nat.card_congr <|
    (Equiv.ofBijective _ <| isComplement_subgroup_left_iff_bijective.mp h).trans <|
      QuotientGroup.quotientRightRelEquivQuotientLeftRel H

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