rightQuotientEquiv — Mathlib

English

A right transversal is in bijection with the set of right cosets of H in G.

Русский

Правый трансверсал биективно эквивалентен множеству правых косет подгруппы H в G.

LaTeX

$$$\\text{rightQuotientEquiv}(hT) : \\Quotient(\\text{QuotientGroup.rightRel } H) \\simeq T$$$

Lean4

/-- A right transversal is in bijection with right cosets. -/
@[to_additive /-- A right transversal is in bijection with right cosets. -/
    ]
noncomputable def rightQuotientEquiv (hT : IsComplement H T) : Quotient (QuotientGroup.rightRel H) ≃ T :=
  (Equiv.ofBijective _ (isComplement_subgroup_left_iff_bijective.mp hT)).symm

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