OAI/NumberTheory/CubicGram/CommonRows.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Exact common-factor row reindexing and matrix decomposition.

  1. def OAI.CubicFirstMoment.residualRows line 16
  2. lemma OAI.CubicFirstMoment.mem_residualRows line 19
  3. lemma OAI.CubicFirstMoment.residualRows_primary line 23
  4. lemma OAI.CubicFirstMoment.primaryPrimeFactors_coprime_overlap line 30
  5. def OAI.CubicFirstMoment.primaryCommonFactor line 47
  6. lemma OAI.CubicFirstMoment.primaryCommonFactor_mul line 50
  7. lemma OAI.CubicFirstMoment.primaryCommonFactor_decomposition line 56
  8. lemma OAI.CubicFirstMoment.primaryCommonFactor_spec line 65
  9. def OAI.CubicFirstMoment.commonRowFactors line 75
  10. lemma OAI.CubicFirstMoment.mem_commonRowFactors line 78
  11. lemma OAI.CubicFirstMoment.commonRowFactors_spec line 82
  12. lemma OAI.CubicFirstMoment.residualRows_image line 91
  13. lemma OAI.CubicFirstMoment.commonFactor_eq_iff_coprime line 101
  14. lemma OAI.CubicFirstMoment.sum_residualRows line 115
  15. lemma OAI.CubicFirstMoment.common_factor_block_reindex line 122
  16. theorem OAI.CubicFirstMoment.common_factor_matrix_decomposition line 177
  17. def OAI.CubicFirstMoment.commonBlockCoefficient line 199
  18. lemma OAI.CubicFirstMoment.commonBlockCoefficient_norm_le line 202
  19. theorem OAI.CubicFirstMoment.primarySmoothedSieveMass_common_blocks line 209