OAI/Combinatorics/Progressions/Linear/FixedAdaptedSymbolFactorizationBasis.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.rational_basis_coordinates_logHeight line 12
  2. theorem OAI.Erdos3.NilpotentLieFiltration.gradedSymbolPolynomial_basis_independent line 51
  3. theorem OAI.Erdos3.NilpotentLieFiltration.symbolPointwiseSubalgebra_basis_independent line 60
  4. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolBasis_change_coordinate line 82
  5. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedBasis_change_coordinate line 93
  6. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedBasis_projection line 101
  7. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGraded_projection_basis_independent line 122
  8. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGraded_submodule_basis_independent line 130
  9. theorem OAI.Erdos3.NilpotentLieFiltration.gradedFrequency_top_basis_independent line 135
  10. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolBasis_change_height line 145
  11. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedBasis_change_height line 156
  12. theorem OAI.Erdos3.NilpotentLieFiltration.native_symbol_basis_independent line 166
  13. def OAI.Erdos3.NilpotentLieFiltration.ControlledSymbolBasisChangeSpec line 183
  14. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlled_symbol_basis_change line 198
  15. def OAI.Erdos3.RationalFilteredNilmanifold.fixedAdaptedSymbolTransferInput line 328
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_fixed_adapted_symbol_factorization_basis line 331