OAI/Combinatorics/Progressions/Linear/DualDerivativeRemoval.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualLogDerivative_sub_tangent_mem line 15
  2. theorem OAI.Erdos3.NilpotentLieFiltration.dualLogDerivative_sub_tangent_mem_layer line 63
  3. theorem OAI.Erdos3.NilpotentLieFiltration.logDerivative_current_layer_relation line 71
  4. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualLogDerivative_one line 94
  5. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualLogDerivative_inv line 97
  6. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualLogDerivative_remove line 106
  7. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualDerivativeSystem_remove line 114
  8. theorem OAI.Erdos3.NilpotentLieFiltration.derivative_removal_preserves_quotient_layers line 135