OAI/Analysis/JiangSu/CentralSequences/ApproximateCentralMatrixSupply.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.NonunitalGamma.ApproximateCentralMatrixUnits line 20
  2. lemma OAI.NonunitalGamma.family_quotient_zero_of_domination line 35
  3. def OAI.NonunitalGamma.modelSequenceEntry line 45
  4. lemma OAI.NonunitalGamma.modelSequenceEntry_apply line 51
  5. lemma OAI.NonunitalGamma.modelSequence_star line 56
  6. lemma OAI.NonunitalGamma.modelSequence_mul line 67
  7. lemma OAI.NonunitalGamma.modelSequence_sum line 89
  8. lemma OAI.NonunitalGamma.modelSequence_commute line 102
  9. theorem OAI.NonunitalGamma.central_matrix_of_finite_models line 111
  10. lemma OAI.NonunitalGamma.contractive_sequence_lift line 155
  11. lemma OAI.NonunitalGamma.family_quotient_zero_eventually line 163
  12. lemma OAI.NonunitalGamma.star_lifts_eventually line 169
  13. lemma OAI.NonunitalGamma.mul_lifts_eventually line 180
  14. lemma OAI.NonunitalGamma.unit_lifts_eventually line 199
  15. lemma OAI.NonunitalGamma.commutator_lifts_eventually line 208
  16. lemma OAI.NonunitalGamma.finite_models_of_matrix_lifts line 222
  17. theorem OAI.NonunitalGamma.finite_models_of_central_matrix line 243