α : Type u
β : Type v
γ : Type w
inst✝² inst✝¹ : Group α
inst✝ : MulAction α β
x : β
y₁ y₂ : α ⧸ stabilizer α x
g₁ g₂ : α
H : g₁ • x = g₂ • x
⊢ g₁⁻¹ * g₂ ∈ stabilizer α x
α : Type u
β : Type v
γ : Type w
inst✝² inst✝¹ : Group α
inst✝ : MulAction α β
x : β
y₁ y₂ : α ⧸ stabilizer α x
g₁ g₂ : α
H : g₁ • x = g₂ • x
⊢ Setoid.r g₁ g₂
rw [leftRel_apply]
α : Type u
β : Type v
γ : Type w
inst✝² inst✝¹ : Group α
inst✝ : MulAction α β
x : β
y₁ y₂ : α ⧸ stabilizer α x
g₁ g₂ : α
H : g₁ • x = g₂ • x
⊢ (g₁⁻¹ * g₂) • x = x
α : Type u
β : Type v
γ : Type w
inst✝² inst✝¹ : Group α
inst✝ : MulAction α β
x : β
y₁ y₂ : α ⧸ stabilizer α x
g₁ g₂ : α
H : g₁ • x = g₂ • x
⊢ g₁⁻¹ * g₂ ∈ stabilizer α x
show (g₁⁻¹ * g₂) • x = x
no goals
α : Type u
β : Type v
γ : Type w
inst✝² inst✝¹ : Group α
inst✝ : MulAction α β
x : β
y₁ y₂ : α ⧸ stabilizer α x
g₁ g₂ : α
H : g₁ • x = g₂ • x
⊢ (g₁⁻¹ * g₂) • x = x
rw [mul_smul, ← H, inv_smul_smul]