OAI/Combinatorics/SumProduct/Alignment/RationalLattice22.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RationalLattice.JointArrays.Component line 34
  2. abbrev OAI.RationalLattice.JointArrays.Carrier line 35
  3. abbrev OAI.RationalLattice.JointArrays.dimension line 36
  4. abbrev OAI.RationalLattice.JointArrays.componentWeight line 37
  5. abbrev OAI.RationalLattice.JointArrays.filtration line 38
  6. abbrev OAI.RationalLattice.JointArrays.lattice line 42
  7. abbrev OAI.RationalLattice.JointArrays.jointWeight line 44
  8. lemma OAI.RationalLattice.JointArrays.covered_geometry line 47
  9. lemma OAI.RationalLattice.JointArrays.filtration_top line 73
  10. lemma OAI.RationalLattice.JointArrays.filtration_terminal line 77
  11. def OAI.RationalLattice.JointArrays.orbit line 82
  12. lemma OAI.RationalLattice.JointArrays.orbit_apply line 88
  13. lemma OAI.RationalLattice.JointArrays.orbit_polynomial line 95
  14. lemma OAI.AllLevelFactorization.covered_factorization_exists line 137
  15. def OAI.AllLevelFactorization.coveredFactorization line 147
  16. def OAI.AllLevelFactorization.coveredResidues line 150
  17. lemma OAI.AllLevelFactorization.covered_quotient_compact line 155
  18. lemma OAI.RationalLattice.JointArrays.factorization_exists line 194
  19. lemma OAI.SourceIntegerArrays.exponent_column_affine line 226
  20. def OAI.SourceIntegerArrays.literalJoint line 251
  21. lemma OAI.SourceIntegerArrays.literalJoint_eq_orbit line 258
  22. theorem OAI.SourceIntegerArrays.literal_joint_factorization line 279