OAI/Algebra/FrobeniusObstruction/Derivations.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.BoundaryOnly.FormalObstruction.Frobenius.relativeDeriv_extline 15 - theorem
OAI.BoundaryOnly.FormalObstruction.Frobenius.partial_include_leftline 44 - theorem
OAI.BoundaryOnly.FormalObstruction.Frobenius.partial_include_left_otherline 70 - theorem
OAI.BoundaryOnly.FormalObstruction.Frobenius.partial_include_rightline 90 - theorem
OAI.BoundaryOnly.FormalObstruction.Frobenius.partial_include_right_otherline 116