OAI/Analysis/JiangSu/CentralSequences/RelativeCentralQuotient.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RelativeCentral.centralizer line 17
  2. instance OAI.RelativeCentral.centralizer_closed line 29
  3. instance OAI.RelativeCentral.(instance at line 33) line 33
  4. instance OAI.RelativeCentral.(instance at line 34) line 34
  5. instance OAI.RelativeCentral.(instance at line 35) line 35
  6. def OAI.RelativeCentral.annihilatorIdeal line 37
  7. lemma OAI.RelativeCentral.mem_annihilator line 61
  8. def OAI.RelativeCentral.annihilator line 65
  9. abbrev OAI.RelativeCentral.Quotient line 85
  10. def OAI.RelativeCentral.quotientMap line 86
  11. lemma OAI.RelativeCentral.quotient_eq_iff line 88
  12. lemma OAI.RelativeCentral.norm_mul_le_quotient line 96
  13. lemma OAI.RelativeCentral.norm_mul_sub_le_quotient line 117
  14. lemma OAI.RelativeCentral.quotient_nontrivial line 123
  15. lemma OAI.RelativeCentral.norm_right_mul_sub_le_quotient line 132