OAI/NumberTheory/DukePrimeDegree/Arithmetic/
204 declarations, 0 contain sorry, 0 declared as axioms; 48 files
Files
- Arithmetic.lean 4 declarations
- ArtinOrders.lean 4 declarations
- ClassFieldBridge.lean 2 declarations
- ClassFieldCongruences.lean 2 declarations
- ClassFieldKernel.lean 2 declarations
- ClassFieldModulus.lean 2 declarations
- ClassFieldRealization.lean 2 declarations
- ConductorModulus.lean 4 declarations
- ConjugateSubfields.lean 6 declarations
- CyclicAverages.lean 2 declarations
- CyclicContinuation.lean 6 declarations
- CyclicFixedOrders.lean 2 declarations
- CyclicGluing.lean 8 declarations
- CyclicInduction.lean 8 declarations
- CyclicIntegerOrders.lean 4 declarations
- CyclicRealCharacters.lean 7 declarations
- CyclicSubfields.lean 6 declarations
- ExceptionalPolynomial.lean 5 declarations
- ExceptionalSetExclusion.lean 1 declarations
- ExceptionalUniverse.lean 1 declarations
- FieldDegree.lean 1 declarations
- FixedFieldTower.lean 4 declarations
- FullLattice.lean 6 declarations
- HeckeFactors.lean 5 declarations
- LatticeBasis.lean 4 declarations
- MultiplierOrder.lean 10 declarations
- NumberFieldResidue.lean 5 declarations
- OrderDiscriminant.lean 11 declarations
- PacketBridge.lean 5 declarations
- PermutationEuler.lean 4 declarations
- PublishedStark.lean 2 declarations
- RationalZeroGap.lean 2 declarations
- ResidueComparison.lean 4 declarations
- StarkAverage.lean 2 declarations
- StarkCharacters.lean 8 declarations
- StarkDescent.lean 6 declarations
- StarkNormalClosure.lean 3 declarations
- StarkOddDegree.lean 2 declarations
- StarkScale.lean 3 declarations
- StarkUnconditional.lean 2 declarations
- StarkZeros.lean 6 declarations
- SubfieldOrders.lean 7 declarations
- UniformResidue.lean 1 declarations
- ZeroPropagation.lean 3 declarations
- ZeroSum.lean 1 declarations
- ZetaCharacterRelations.lean 4 declarations
- ZetaIsomorphism.lean 6 declarations
- ZetaOrder.lean 9 declarations