def YoungDiagram.Cell (μ : YoungDiagram) : Type

Equations

• μ.Cell = ↥μ.cells

instance instFintypeCell (μ : YoungDiagram) : Fintype μ.Cell

Equations

• instFintypeCell μ = inferInstanceAs (Fintype ↥μ.cells)

instance instDecidableEqCell (μ : YoungDiagram) : DecidableEq μ.Cell

Equations

• instDecidableEqCell μ = inferInstanceAs (DecidableEq ↥μ.cells)

def YoungDiagram.toSimpleGraph (μ : YoungDiagram) : SimpleGraph μ.Cell

The simple graph of a Young diagram: two distinct cells are adjacent iff they lie in the same row or in the same column.

Equations

• μ.toSimpleGraph = SimpleGraph.fromRel fun (a b : μ.Cell) => (↑a).1 = (↑b).1 ∨ (↑a).2 = (↑b).2