card_quotient_rightRel — Mathlib

English

There is a natural bijection between α and α modulo the bottom subgroup ⊥.

Русский

Существует естественная биекция между α и α по факторгруппе от нулевой подгруппы ⊥.

LaTeX

$$$\\α / (⊥) \\cong α$$$

Lean4

@[to_additive]
theorem card_quotient_rightRel [Fintype (α ⧸ s)] :
    Fintype.card (Quotient (QuotientGroup.rightRel s)) = Fintype.card (α ⧸ s) :=
  Fintype.ofEquiv_card (QuotientGroup.quotientRightRelEquivQuotientLeftRel s).symm

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