OddSubfields.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Proper subfields in every odd extension degree. The degree divisor and its properness are derived from actual finite-field cardinalities, not assumed of the splitting field chosen by the construction.

theorem OAI.RyserCoveringCounterexample.three_mul_le_of_dvd_odd line 15
Source documentation
A proper divisor of a positive odd number has index at least three.
```
theorem three_mul_le_of_dvd_odd {d n : ℕ} (hn : Odd n) (hd : d ∣ n)
    (hne : d ≠ n) : 3 * d ≤ n := by
…
```
theorem OAI.RyserCoveringCounterexample.subfield_degree_data_of_odd line 42
Source documentation
The actual degree of a proper subfield divides the odd ambient degree and is at most one third of it. No primality assumption on the degree is used.
```
theorem subfield_degree_data_of_odd (hp : p.Prime) (hn : Odd n)
    (hcard : Fintype.card F = p ^ n) (S : Subfield F) [Fintype S]
    (hS : S ≠ ⊤) :
    ∃ d : ℕ, 0 < d ∧ d ∣ n ∧ 3 * d ≤ n ∧ Fintype.card S = p ^ d := by
…
```

theorem OAI.RyserCoveringCounterexample.subfield_card_cube_le_of_odd_degree line 66

Source documentation

Cube bound for proper subfields in arbitrary odd degree, including composite degree.

theorem subfield_card_cube_le_of_odd_degree (hp : p.Prime) (hn : Odd n)
    (hcard : Fintype.card F = p ^ n) (S : Subfield F) [Fintype S]
    (hS : S ≠ ⊤) : Fintype.card S ^ 3 ≤ Fintype.card F := by
…

theorem OAI.RyserCoveringCounterexample.subfield_natCard_cube_le_of_odd_degree line 74

Source documentation

Choice-free cardinal version of the arbitrary odd-degree cube bound.

theorem subfield_natCard_cube_le_of_odd_degree (hp : p.Prime) (hn : Odd n)
    (hcard : Fintype.card F = p ^ n) (S : Subfield F) (hS : S ≠ ⊤) :
    Nat.card S ^ 3 ≤ Fintype.card F := by
…

theorem OAI.RyserCoveringCounterexample.extensionField_properSubfield_cube_le_of_odd line 84
Source documentation
The constructed splitting field satisfies the required cube bound for every odd degree above two, with no hypothesis on its proper subfields.
```
theorem extensionField_properSubfield_cube_le_of_odd (p n : ℕ) [Fact p.Prime]
    (hn : Odd n) (_hn3 : 2 < n) (S : Subfield (ExtensionField p n)) (hS : S ≠ ⊤) :
    Nat.card S ^ 3 ≤ Fintype.card (ExtensionField p n) := by
…
```
Mentions: OAI.RyserCoveringCounterexample.ExtensionField
theorem OAI.RyserCoveringCounterexample.extensionField_properSubfield_cube_le_pow_of_odd line 92
Source documentation
Same bound with the actual ambient cardinality written as its prime power.
```
theorem extensionField_properSubfield_cube_le_pow_of_odd (p n : ℕ) [Fact p.Prime]
    (hn : Odd n) (hn3 : 2 < n) (S : Subfield (ExtensionField p n)) (hS : S ≠ ⊤) :
    Nat.card S ^ 3 ≤ p ^ n := by
…
```
Mentions: OAI.RyserCoveringCounterexample.ExtensionField