transpose_eq_iff

Mathlib.Combinatorics.Young.YoungDiagram

URI: https://scilib.ai/kg/mathlib#YoungDiagram.transpose_eq_iff

← MathLib Explorer

English

μ.transpose = ν.transpose iff μ = ν.

Русский

μ.transpose = ν.transpose эквивалентно μ = ν.

LaTeX

$$$ μ^{\top} = ν^{\top} \iff μ = ν. $$$

Lean4

@[simp]
theorem transpose_eq_iff {μ ν : YoungDiagram} : μ.transpose = ν.transpose ↔ μ = ν :=
  by
  rw [transpose_eq_iff_eq_transpose]
  simp
    -- This is effectively both directions of `transpose_le_iff` below.

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru