OAI/NumberTheory/PiExponent/LocalAlgebra/ConeComplex.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponentSiegelAux.W30.coneBottom_comp line 12
2. def OAI.PiExponentSiegelAux.W30.scalarConeObject line 22
3. def OAI.PiExponentSiegelAux.W30.scalarConeMap line 26
4. lemma OAI.PiExponentSiegelAux.W30.chain_linear_comp_zero line 32
5. theorem OAI.PiExponentSiegelAux.W30.scalarConeMap_comp line 37
6. def OAI.PiExponentSiegelAux.W30.scalarConeComplex line 48
7. theorem OAI.PiExponentSiegelAux.W30.scalarCone_interior_exact line 52