injective_ofQuotientStabilizer — Mathlib

English

The map of quotient stabilizers is injective: if two elements of α map to the same coset, they are equal in the quotient stabilizer sense.

Русский

Карта факторного стабилизатора инъективна: если два элемента α имеют одинаковый образ, то они равны в рамках стабилизатора.

LaTeX

$$Injective((ofQuotientStabilizer): α × HasQuotient.Quotient α (MulAction.stabilizer α x) → β)$$

Lean4

@[to_additive]
theorem injective_ofQuotientStabilizer : Function.Injective (ofQuotientStabilizer α x) := fun y₁ y₂ =>
  Quotient.inductionOn₂' y₁ y₂ fun g₁ g₂ (H : g₁ • x = g₂ • x) =>
    Quotient.sound' <| by
      rw [leftRel_apply]
      change (g₁⁻¹ * g₂) • x = x
      rw [mul_smul, ← H, inv_smul_smul]

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