Basic.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Saxl.intertwining_finrank_pos_iff line 14

Source comment

The genuine finite-dimensional Hom criterion; no simplicity hypothesis.

theorem intertwining_finrank_pos_iff {G : Type uG} {V : Type uV} {W : Type uW} [Group G]
    [AddCommGroup V] [AddCommGroup W] [Module ℂ V] [Module ℂ W]
    [Module.Finite ℂ V] [Module.Finite ℂ W]
    (ρ : Representation ℂ G V) (σ : Representation ℂ G W) :
    0 < Module.finrank ℂ (Representation.IntertwiningMap ρ σ) ↔
      ∃ f : Representation.IntertwiningMap ρ σ, f ≠ 0 :=
…

theorem OAI.Saxl.kronecker_pos_iff line 22
theorem OAI.Saxl.column_perm_rowWord line 32
Source comment
Column permutations cannot also fix the row word unless they are identity.
```
theorem column_perm_rowWord {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ)
    (g : columnGroup t) (hg : rowWord t ∘ (g : Equiv.Perm (Fin n)) = rowWord t) :
    g = 1 := by
…
```
Mentions: OAI.Saxl.Tableau, OAI.Saxl.columnGroup, OAI.Saxl.rowWord
theorem OAI.Saxl.polytabloid_rowWord line 45
Source comment
The coefficient of the canonical row word in its polytabloid is one.
```
theorem polytabloid_rowWord {n : ℕ} {μ : YoungDiagram} (t : Tableau n μ) :
    polytabloid t (rowWord t) = 1 := by
…
```
Mentions: OAI.Saxl.Tableau, OAI.Saxl.polytabloid, OAI.Saxl.rowWord
theorem OAI.Saxl.mem_staircase line 60
theorem OAI.Saxl.staircase_cells_succ line 67
theorem OAI.Saxl.staircase_card_succ line 75
theorem OAI.Saxl.staircase_card_zero line 87
theorem OAI.Saxl.staircase_card_double line 90
theorem OAI.Saxl.staircase_card line 99
Source comment
The staircase has triangular cardinality.
```
theorem staircase_card (m : ℕ) : (staircase m).card = m * (m + 1) / 2 := by
…
```
Mentions: OAI.Saxl.staircase