OAI/Combinatorics/Progressions/Linear/AssociatedGradedBasisIndependence.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.gradedPieceProjection line 16
  2. theorem OAI.Erdos3.NilpotentLieFiltration.gradedPieceProjection_coordinate line 20
  3. theorem OAI.Erdos3.NilpotentLieFiltration.gradedPieceProjection_eq_pieceMap line 26
  4. theorem OAI.Erdos3.NilpotentLieFiltration.gradedRefiltrationLayer_eq_inf_comap line 33
  5. theorem OAI.Erdos3.NilpotentLieFiltration.real_gradedPieceProjection_coordinate line 44
  6. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomial_coefficient_of_polynomial line 57
  7. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedPieceMap_repr_symm line 86
  8. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedBasis_repr_symm_eq_projection line 95
  9. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedBasis_repr_change line 103
  10. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedBasis_projection_pieceMap line 127
  11. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedBasis_projection_independent line 137
  12. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedBasis_gradedSubmodule_independent line 148