leftRel_r_eq_leftCosetEquivalence

English

The left relation on the quotient equals the equivalence relation of sharing a left coset.

Русский

Левое отношение на фактор-группе совпадает с эквивалентностью по общей левой косете.

LaTeX

$$$\text{LeftRel}(s) = \text{LeftCosetEquivalence}(s)$$$

Lean4

theorem leftRel_r_eq_leftCosetEquivalence : ⇑(QuotientGroup.leftRel s) = LeftCosetEquivalence s :=
  by
  ext
  rw [leftRel_eq]
  exact (leftCoset_eq_iff s).symm

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