OAI/Combinatorics/Progressions/Polynomial/RealGradedSymbolPolynomial.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.mixedCoordinates line 18
  2. theorem OAI.Erdos3.VectorPolynomial.mixedCoordinates_apply line 23
  3. theorem OAI.Erdos3.VectorPolynomial.mixedCoordinates_symm_apply line 27
  4. def OAI.Erdos3.VectorPolynomial.ofSupportedCoordinates line 33
  5. theorem OAI.Erdos3.VectorPolynomial.ofSupportedCoordinates_apply line 37
  6. theorem OAI.Erdos3.VectorPolynomial.ofSupportedCoordinates_apply_of_not_mem line 44
  7. def OAI.Erdos3.VectorPolynomial.supportedCoordinates line 54
  8. theorem OAI.Erdos3.VectorPolynomial.supportedCoordinates_apply line 58
  9. theorem OAI.Erdos3.VectorPolynomial.supportedCoordinates_ofSupportedCoordinates line 62
  10. def OAI.Erdos3.VectorPolynomial.realificationLinearEquiv line 82
  11. theorem OAI.Erdos3.VectorPolynomial.coefficients_realificationLinearEquiv_tmul line 86
  12. theorem OAI.Erdos3.VectorPolynomial.realificationLinearEquiv_eq_zero_iff line 96
  13. theorem OAI.Erdos3.VectorPolynomial.ring_zero_lie line 114
  14. theorem OAI.Erdos3.VectorPolynomial.ring_lie_zero line 116
  15. def OAI.Erdos3.VectorPolynomial.lieTensorLeftComm line 121
  16. def OAI.Erdos3.VectorPolynomial.realificationLieEquiv line 145
  17. theorem OAI.Erdos3.VectorPolynomial.realificationLieEquiv_tmul_tmul line 149
  18. theorem OAI.Erdos3.VectorPolynomial.coefficients_realificationLieEquiv_tmul line 153
  19. theorem OAI.Erdos3.VectorPolynomial.eval_realificationLieEquiv_tmul line 173
  20. instance OAI.Erdos3.VectorPolynomial.realModule line 195
  21. def OAI.Erdos3.VectorPolynomial.realificationRealLinearEquiv line 198
  22. theorem OAI.Erdos3.VectorPolynomial.realificationRealLinearEquiv_apply line 202
  23. instance OAI.Erdos3.VectorPolynomial.realScalarTower line 206
  24. theorem OAI.Erdos3.VectorPolynomial.coefficients_realification_smul line 209
  25. theorem OAI.Erdos3.VectorPolynomial.coefficients_smul_real line 220
  26. def OAI.Erdos3.VectorPolynomial.realCoefficient line 227
  27. theorem OAI.Erdos3.VectorPolynomial.realCoefficient_apply line 233
  28. def OAI.Erdos3.VectorPolynomial.realMonomial line 236
  29. theorem OAI.Erdos3.VectorPolynomial.realMonomial_apply line 248
  30. theorem OAI.Erdos3.VectorPolynomial.realificationLieEquiv_smul line 257
  31. instance OAI.Erdos3.VectorPolynomial.realLieAlgebra line 262
  32. theorem OAI.Erdos3.linear_map_lie_of_basis line 287
  33. theorem OAI.Erdos3.VectorPolynomial.ofSupportedCoordinates_single line 301
  34. def OAI.Erdos3.NilpotentLieFiltration.gradedSymbolPolynomial line 328
  35. theorem OAI.Erdos3.NilpotentLieFiltration.gradedSymbolPolynomial_coefficient line 334
  36. theorem OAI.Erdos3.NilpotentLieFiltration.gradedSymbolPolynomial_coefficient_of_ne line 346
  37. theorem OAI.Erdos3.NilpotentLieFiltration.gradedSymbolPolynomial_basis line 357
  38. theorem OAI.Erdos3.NilpotentLieFiltration.gradedSymbolPolynomial_injective line 365
  39. theorem OAI.Erdos3.NilpotentLieFiltration.gradedSymbolPolynomial_lie_basis line 372
  40. def OAI.Erdos3.NilpotentLieFiltration.gradedSymbolPolynomialLie line 408
  41. def OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomial line 437
  42. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomial_coefficient_tmul line 442
  43. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomial_coordinate line 452
  44. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomial_coordinate_of_ne line 463
  45. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomial_injective line 473
  46. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomial_map_coefficient line 480