OAI/Algebra/FrobeniusObstruction/
709 declarations, 0 contain sorry, 0 declared as axioms; 35 files
Files
- ActualBlocks.lean 26 declarations
- BlockCohomology.lean 15 declarations
- BlockPairing.lean 23 declarations
- BlockTensor.lean 34 declarations
- ChartPairing.lean 35 declarations
- CoordinateMaps.lean 8 declarations
- Coordinates.lean 13 declarations
- CycleTransfer.lean 3 declarations
- Derivations.lean 5 declarations
- ExteriorSplit.lean 6 declarations
- FixedResidue.lean 14 declarations
- FormTensor.lean 31 declarations
- FormalData.lean 21 declarations
- FrobeniusRing.lean 71 declarations
- GlobalForms.lean 25 declarations
- GraphPotential.lean 26 declarations
- LiftProducts.lean 14 declarations
- LinearChange.lean 32 declarations
- MixedForms.lean 55 declarations
- MovingCharts.lean 28 declarations
- NilpotentInverse.lean 4 declarations
- NormalPrimitives.lean 43 declarations
- Obstruction.lean 2 declarations
- ParameterLifts.lean 8 declarations
- ResiduePairing.lean 26 declarations
- Retractions.lean 3 declarations
- SelectedCycles.lean 12 declarations
- SignedTensor.lean 15 declarations
- SquareZero.lean 26 declarations
- TangentCharts.lean 23 declarations
- TensorCohomology.lean 7 declarations
- TensorKernels.lean 5 declarations
- ThreeParameters.lean 19 declarations
- TopResidue.lean 16 declarations
- VanishingIdeals.lean 15 declarations