OAI/NumberTheory/PiExponent/Jets/ResidueConormalPairing.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.PiExponentSiegel.W58.cotangentQuotientScalarTower line 11
2. def OAI.PiExponentSiegel.W58.residueConormalPairing line 14
3. theorem OAI.PiExponentSiegel.W58.residueConormalPairing_apply line 18
4. theorem OAI.PiExponentSiegel.W58.residueConormalPairing_toCotangent line 21
5. theorem OAI.PiExponentSiegel.W58.residueConormalPairing_restrictScalars line 24
6. def OAI.PiExponentSiegel.W58.reducedDerivation line 29
7. theorem OAI.PiExponentSiegel.W58.reducedDerivation_apply line 32
8. def OAI.PiExponentSiegel.W58.derivationNormal line 35
9. theorem OAI.PiExponentSiegel.W58.derivationNormal_toCotangent line 38