OAI/Combinatorics/Progressions/Estimates/StepDropTerminalContainment.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.stepDropBracketKernel line 14
  2. def OAI.Erdos3.stepDropSubmodule line 26
  3. theorem OAI.Erdos3.mem_stepDropSubmodule line 32
  4. theorem OAI.Erdos3.basisGradeProjection_one_lie_eq_zero line 39
  5. theorem OAI.Erdos3.stepDropSubmodule_lie_mem line 55
  6. def OAI.Erdos3.stepDropSubalgebra line 88
  7. theorem OAI.Erdos3.stepDropSubmodule_graded line 96
  8. theorem OAI.Erdos3.stepDropSubmodule_mem_higher_grade line 125
  9. def OAI.Erdos3.rightLieLinear line 156
  10. theorem OAI.Erdos3.rightLieLinear_apply line 161
  11. theorem OAI.Erdos3.stepDropBracketKernel_eq_iInf line 164
  12. theorem OAI.Erdos3.rightLieLinear_baseChange line 186
  13. theorem OAI.Erdos3.stepDropBracketKernel_baseChange line 196
  14. theorem OAI.Erdos3.stepDropSubmodule_baseChange line 212
  15. def OAI.Erdos3.homogeneousIntersection line 235
  16. theorem OAI.Erdos3.mem_homogeneousIntersection line 239
  17. theorem OAI.Erdos3.homogeneousIntersection_finrank_le line 246
  18. theorem OAI.Erdos3.homogeneousIntersection_baseChange line 254
  19. abbrev OAI.Erdos3.StepDropRow line 273
  20. def OAI.Erdos3.stepDropSystem line 277
  21. theorem OAI.Erdos3.stepDrop_quotient_mem_iff line 290
  22. theorem OAI.Erdos3.stepDropSystem_ker line 304
  23. theorem OAI.Erdos3.stepDropSystem_basis_height line 333
  24. theorem OAI.Erdos3.stepDropSubmodule_top_frequency line 376
  25. theorem OAI.Erdos3.NilpotentLieFiltration.FormalInductionRun.terminal_coefficients_mem_stepDropSubmodule line 397
  26. theorem OAI.Erdos3.NilpotentLieFiltration.FormalInductionRun.terminal_coefficients_mem_rational_stepDrop line 417
  27. theorem OAI.Erdos3.NilpotentLieFiltration.FormalInductionRun.terminal_log_mem_stepDropSubalgebra line 426