OAI/Algebra/OddKaplansky/HeisenbergSector.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OddKaplansky.Heisenberg.Sector line 13
  2. lemma OAI.OddKaplansky.Heisenberg.mem_sector_of_fixed line 14
  3. lemma OAI.OddKaplansky.Heisenberg.fixed_of_mem_sector line 16
  4. lemma OAI.OddKaplansky.Heisenberg.Ω_fixed line 21
  5. def OAI.OddKaplansky.Heisenberg.frame line 24
  6. lemma OAI.OddKaplansky.Heisenberg.f_single line 25
  7. lemma OAI.OddKaplansky.Heisenberg.span_frame line 33
  8. lemma OAI.OddKaplansky.Heisenberg.sector_dim_le line 46
  9. def OAI.OddKaplansky.Heisenberg.encode line 50
  10. lemma OAI.OddKaplansky.Heisenberg.encode_apply line 54
  11. lemma OAI.OddKaplansky.Heisenberg.encode_fixed line 56
  12. lemma OAI.OddKaplansky.Heisenberg.ρ_encode line 59
  13. lemma OAI.OddKaplansky.Heisenberg.encode_injective line 64
  14. lemma OAI.OddKaplansky.Heisenberg.encode_range line 69
  15. lemma OAI.OddKaplansky.Heisenberg.ρ_injective_on_sector line 76
  16. lemma OAI.OddKaplansky.Heisenberg.Ω_mul line 84
  17. lemma OAI.OddKaplansky.Heisenberg.Ω_sum line 97
  18. lemma OAI.OddKaplansky.Heisenberg.Ω_ne_zero line 107
  19. lemma OAI.OddKaplansky.Heisenberg.encode_mul line 113