SlabPartition.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.KaplanskyCounterexample.FiniteGeometry.NoEigenvector line 14
lemma OAI.KaplanskyCounterexample.FiniteGeometry.independent_pair_of_noEigenvector line 17
theorem OAI.KaplanskyCounterexample.FiniteGeometry.existsUnique_slab_functional line 22
def OAI.KaplanskyCounterexample.FiniteGeometry.slabLine line 40
lemma OAI.KaplanskyCounterexample.FiniteGeometry.slabLine_off_axis line 43
lemma OAI.KaplanskyCounterexample.FiniteGeometry.slabLine_functional_ne_zero line 50
theorem OAI.KaplanskyCounterexample.FiniteGeometry.slab_partition line 58
Source documentation
The axis and the displayed lifted lines partition the slab.
```
theorem slab_partition [FiniteDimensional Q P] (hd : finrank Q P = 2)
    (J : P →ₗ[Q] P) (hJ : NoEigenvector J) (p : P × Q) :
    p.1 = 0 ∨ ∃! γ : {γ : P →ₗ[Q] Q // γ ≠ 0}, p ∈ slabLine J γ.val := by
…
```
Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.NoEigenvector, OAI.KaplanskyCounterexample.FiniteGeometry.slabLine
theorem OAI.KaplanskyCounterexample.FiniteGeometry.slabLine_is_line line 73
Source documentation
The displayed set is a full affine line, not merely an arbitrary part of the partition; its direction has nonzero projection to the plane.
```
theorem slabLine_is_line [FiniteDimensional Q P] (hd : finrank Q P = 2)
    (J : P →ₗ[Q] P) (γ : P →ₗ[Q] Q) (hγ : γ ≠ 0) :
    ∃ u v : P × Q, v.1 ≠ 0 ∧
      slabLine J γ = Set.range (fun t : Q => u + t • v) := by
…
```
Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.slabLine
theorem OAI.KaplanskyCounterexample.FiniteGeometry.exists_noEigenvector_of_quadratic line 129
Source documentation
A quadratic extension supplies the operator without eigenvectors.
```
theorem exists_noEigenvector_of_quadratic (hd : finrank Q F = 2) :
    ∃ J : F →ₗ[Q] F, NoEigenvector J := by
…
```
Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.NoEigenvector