σ : Type u_1
R : Type u_2
τ : Type ?u.175098
S : Type ?u.175101
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e✝ : Perm σ
⊢ ↑(rename ↑e✝) (esymm σ R n) = esymm σ R n
σ : Type u_1
R : Type u_2
τ : Type ?u.175098
S : Type ?u.175101
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
⊢ IsSymmetric (esymm σ R n)
intro
no goals
σ : Type u_1
R : Type u_2
τ : Type ?u.175098
S : Type ?u.175101
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e✝ : Perm σ
⊢ ↑(rename ↑e✝) (esymm σ R n) = esymm σ R n
rw [rename_esymm]