OAI/RingTheory/DirectFiniteness/QuotientField.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.Prescription.irreducibleCoeffs line 15
2. lemma OAI.KaplanskyCounterexample.Prescription.irreducibleCoeffs_exists line 18
3. def OAI.KaplanskyCounterexample.Prescription.firstCoeffs line 29
4. def OAI.KaplanskyCounterexample.Prescription.firstPolynomial line 32
5. lemma OAI.KaplanskyCounterexample.Prescription.firstPolynomial_monic line 34
6. lemma OAI.KaplanskyCounterexample.Prescription.firstPolynomial_degree line 36
7. lemma OAI.KaplanskyCounterexample.Prescription.firstPolynomial_irreducible line 38
8. lemma OAI.KaplanskyCounterexample.Prescription.firstCoeffs_le line 40
9. abbrev OAI.KaplanskyCounterexample.Prescription.CoefficientField line 46

   Source documentation

   Exactly F₂[Z]/(g), with g the lexicographically first monic irreducible polynomial of the prescribed degree.

   abbrev CoefficientField (d : ℕ) (hd : 0 < d) := AdjoinRoot (firstPolynomial d hd)

   Mentions: OAI.KaplanskyCounterexample.Prescription.firstPolynomial

10. instance OAI.KaplanskyCounterexample.Prescription.firstPolynomial_fact line 48
11. instance OAI.KaplanskyCounterexample.Prescription.coefficientField_finite line 51
12. instance OAI.KaplanskyCounterexample.Prescription.coefficientField_fintype line 56
13. lemma OAI.KaplanskyCounterexample.Prescription.coefficientField_finrank line 59
14. lemma OAI.KaplanskyCounterexample.Prescription.coefficientField_card line 64
15. def OAI.KaplanskyCounterexample.Prescription.coefficientFieldOrder line 68