μ ν : YoungDiagram
⊢ μ = transpose (transpose ν) ↔ μ = ν
μ ν : YoungDiagram
⊢ transpose μ = transpose ν ↔ μ = ν
rw [transpose_eq_iff_eq_transpose]
no goals
μ ν : YoungDiagram
⊢ μ = transpose (transpose ν) ↔ μ = ν
simp