OAI/Algebra/OddKaplansky/CoefficientOrder.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OddKaplansky.QuadraticTower.firstCoordinates line 10
2. def OAI.OddKaplansky.QuadraticTower.secondCoordinates line 12
3. def OAI.OddKaplansky.QuadraticTower.coefficientTuple line 15
4. lemma OAI.OddKaplansky.QuadraticTower.coefficientTuple_injective line 20
5. def OAI.OddKaplansky.QuadraticTower.fieldOrder line 32