transposeOrderIso — Mathlib

English

Transposing Young diagrams defines an order isomorphism from YoungDiagram to YoungDiagram.

Русский

Транспонирование диаграмм Юнга задаёт упорядочивающее изоморфизм между диаграммами Юнга.

LaTeX

$$$ \mathrm{transposeOrderIso} : \mathrm{YoungDiagram} \cong_o \mathrm{YoungDiagram}. $$$

Lean4

/-- Transposing Young diagrams is an `OrderIso`. -/
@[simps]
def transposeOrderIso : YoungDiagram ≃o YoungDiagram :=
  ⟨⟨transpose, transpose, fun _ => by simp, fun _ => by simp⟩, by simp⟩

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