orbit_inj — Mathlib

English

Variant of quotient equality under a subgroup when mk'' is used instead of mk.

Русский

Вариант равенства классов по подгруппе при использовании mk'' вместо mk.

LaTeX

$$(h : (Quotient.mk'' a) = (Quotient.mk'' b)) ⇒ ((Quotient.mk'' a) = (Quotient.mk'' b))$$

Lean4

@[to_additive (attr := simp)]
theorem orbit_inj {x y : orbitRel.Quotient G α} : x.orbit = y.orbit ↔ x = y :=
  orbitRel.Quotient.orbit_injective.eq_iff

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