OAI/Combinatorics/Progressions/Estimates/RealSubquotientEquiv.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.one_tmul_mem_real_baseChange_iff line 19
  2. theorem OAI.Erdos3.real_baseChange_iSup line 48
  3. theorem OAI.Erdos3.real_restrictScalars_iSup line 67
  4. theorem OAI.Erdos3.realification_subtype_injective line 96
  5. def OAI.Erdos3.realificationSubmoduleEquiv line 102
  6. theorem OAI.Erdos3.realificationSubmoduleEquiv_coe line 106
  7. theorem OAI.Erdos3.realificationSubmoduleEquiv_tmul line 109
  8. theorem OAI.Erdos3.realification_ker line 125
  9. theorem OAI.Erdos3.realification_comap line 132
  10. theorem OAI.Erdos3.realification_mkQ_eq_zero_iff line 139
  11. theorem OAI.Erdos3.realification_prod line 144
  12. theorem OAI.Erdos3.realification_prod_eq_zero_iff line 151
  13. abbrev OAI.Erdos3.RealSubquotient line 176
  14. def OAI.Erdos3.realSubquotientProjection line 181
  15. theorem OAI.Erdos3.realSubquotientProjection_surjective line 184
  16. theorem OAI.Erdos3.realSubquotientProjection_ker line 189
  17. def OAI.Erdos3.realSubquotientEquiv line 200
  18. theorem OAI.Erdos3.realSubquotientEquiv_project line 206