OAI/Algebra/FrobeniusObstruction/NilpotentInverse.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoundaryOnly.FormalObstruction.NilpotentInverse.difference_pow line 14
2. theorem OAI.BoundaryOnly.FormalObstruction.NilpotentInverse.injective_of_first_jet line 42
3. theorem OAI.BoundaryOnly.FormalObstruction.NilpotentInverse.bijective_of_first_jet line 59
4. theorem OAI.BoundaryOnly.FormalObstruction.NilpotentInverse.first_jet_of_generators line 67