OAI/Algebra/FrobeniusObstruction/CoordinateMaps.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoundaryOnly.FormalObstruction.Frobenius.mapCoefficients line 14
2. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.mapCoefficients_mk line 26
3. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.mapCoefficients_coordinate line 31
4. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.mapCoefficients_monomial line 36
5. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.coefficients_mapCoefficients line 41
6. def OAI.BoundaryOnly.FormalObstruction.Frobenius.monomialBasis line 48
7. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.monomialBasis_apply line 51
8. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.monomialBasis_repr line 60