α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ : Perm α
h : swap i j * σ = σ
swap_id : swap i j = 1
⊢ i = j
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ : Perm α
h : swap i j * σ = σ
⊢ i = j
have swap_id : swap i j = 1 := mul_right_cancel (_root_.trans h (one_mul σ).symm)
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ : Perm α
h : swap i j * σ = σ
swap_id : swap i j = 1
⊢ ↑1 j = j
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ : Perm α
h : swap i j * σ = σ
swap_id : swap i j = 1
⊢ i = j
rw [← swap_apply_right i j, swap_id]
no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ : Perm α
h : swap i j * σ = σ
swap_id : swap i j = 1
⊢ ↑1 j = j
rfl
no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ : Perm α
h : i = j
⊢ swap i j * σ = σ
erw [h, swap_self, one_mul]