OAI/Combinatorics/Progressions/Linear/SquarefreeBasisPermutation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.MultidegreeLieFiltration.squarefreeBasis line 18
  2. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeBasis_repr line 21
  3. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeBasis_coefficient_self line 25
  4. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeBasis_coefficient_ne line 32
  5. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeBasis_monomial line 39
  6. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeSupport_eq_span line 64
  7. def OAI.Erdos3.MultidegreeLieFiltration.squarefreeSupportedBasis line 80
  8. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeSupportedBasis_coe line 85
  9. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeCoefficientLayer_permute line 103
  10. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeBasis_permute line 110