OAI/Algebra/OddKaplansky/Main.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OddKaplansky.Prescribed.K line 14
  2. instance OAI.OddKaplansky.Prescribed.(instance at line 15) line 15
  3. instance OAI.OddKaplansky.Prescribed.(instance at line 17) line 17
  4. instance OAI.OddKaplansky.Prescribed.(instance at line 18) line 18
  5. instance OAI.OddKaplansky.Prescribed.(instance at line 19) line 19
  6. lemma OAI.OddKaplansky.Prescribed.card_field line 22
  7. def OAI.OddKaplansky.Prescribed.zeta line 24
  8. lemma OAI.OddKaplansky.Prescribed.zeta_primitive line 25
  9. lemma OAI.OddKaplansky.Prescribed.zeta_le line 30
  10. def OAI.OddKaplansky.Prescribed.localDatum line 36
  11. def OAI.OddKaplansky.Prescribed.rectangles line 37
  12. abbrev OAI.OddKaplansky.Prescribed.G line 38
  13. def OAI.OddKaplansky.Prescribed.a line 39
  14. def OAI.OddKaplansky.Prescribed.b line 40
  15. lemma OAI.OddKaplansky.Prescribed.products line 41
  16. lemma OAI.OddKaplansky.Prescribed.torsion line 42
  17. lemma OAI.OddKaplansky.Prescribed.cellular_consequences line 43
  18. def OAI.OddKaplansky.cellular line 63

    Also declared: ComparatorChallenges/OddKaplansky.lean:12 (same declaration text).

  19. lemma OAI.OddKaplansky.cellular_eq_operator line 66
  20. def OAI.OddKaplansky.MainClaim line 71

    Also declared: ComparatorChallenges/OddKaplansky.lean:16 (same declaration text).

  21. theorem OAI.OddKaplansky.main_theorem line 81

    Distinct definitions of this name: ComparatorChallenges/OddKaplansky.lean:26 (same statement text; different proof or body). Qualify references as OAI.OddKaplansky.main_theorem@path.

  22. theorem OAI.OddKaplansky.fixed_field_transfer line 92