English
If α is finite, then the quotient by the rightRel relation on s is finite and in bijection with α ⧸ s.
Русский
Если α конечно, фактор по правойRelation на s конечен и взаимно однозначно сопоставим α ⧸ s.
LaTeX
$$$[Fintype (α/ s)] \\Rightarrow Fintype.card (Quotient (QuotientGroup.rightRel s)) = Fintype.card (α/ s)$$$
Lean4
/-- `α ⧸ ⊥` is in bijection with `α`. See `QuotientGroup.quotientBot` for a multiplicative
version. -/
@[to_additive /-- `α ⧸ ⊥` is in bijection with `α`. See `QuotientAddGroup.quotientBot` for an
additive version. -/
]
def quotientEquivSelf : α ⧸ (⊥ : Subgroup α) ≃ α
where
toFun :=
Quotient.lift id <| fun x y (h : leftRel ⊥ x y) ↦
eq_of_inv_mul_eq_one <| by rwa [leftRel_apply, Subgroup.mem_bot] at h
invFun := QuotientGroup.mk
left_inv x := by induction x using Quotient.inductionOn; simp
right_inv x := by simp
