OAI/Combinatorics/Progressions/Linear/LieKernelRealificationMark.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.mem_realificationLieKernel_iff line 13
2. theorem OAI.Erdos3.realificationLieSubalgebra_ker line 18
3. theorem OAI.Erdos3.NilpotentLieBCHGroup.coord_mem_realificationKernel_iff line 30
4. theorem OAI.Erdos3.NilpotentLieBCHGroup.mem_realificationSubgroup_ker_iff line 41
5. theorem OAI.Erdos3.NilpotentLieBCHGroup.realificationSubgroup_ker line 48
6. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_realificationKernel_lift line 54