OAI/Combinatorics/Progressions/Linear/LieWordProjection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.lieWordSubalgebra line 11
2. theorem OAI.Erdos3.commutatorTree_mem_lieWordSubalgebra line 15
3. theorem OAI.Erdos3.freeLieWordExpansion_range line 21
4. def OAI.Erdos3.lieWordProjection line 41
5. theorem OAI.Erdos3.lieWordProjection_apply line 44
6. theorem OAI.Erdos3.lieWordProjection_idempotent line 47
7. theorem OAI.Erdos3.lieWordProjection_eq_self_iff line 51