OAI/Combinatorics/Progressions/Estimates/FreeWeightedEvaluationBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.FreeNilpotentLieAlgebra.lift_weightedLayer line 14
2. def OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.lift line 23
3. theorem OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.lift_mk line 30
4. theorem OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.lift_of line 33
5. theorem OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.lift_mem_layer line 36
6. theorem OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.hom_ext line 41
7. theorem OAI.Erdos3.FreeWeightedNilpotentLieAlgebra.lift_basis_matrix_logHeight line 65