OAI/NumberTheory/PiExponent/Jets/ConormalPairing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentSiegel.W58.ideal_smul_quotient_zero line 12
2. def OAI.PiExponentSiegel.W58.normalRestriction line 17
3. theorem OAI.PiExponentSiegel.W58.normalRestriction_product_zero line 24
4. def OAI.PiExponentSiegel.W58.conormalPairing line 28
5. theorem OAI.PiExponentSiegel.W58.conormalPairing_toCotangent line 31