OAI/NumberTheory/SiegelZeros/Characters/
310 declarations, 0 contain sorry, 0 declared as axioms; 32 files
Files
- AuxiliarySqrtPairCharacterField.lean 1 declarations
- Biquadratic.lean 7 declarations
- BiquadraticArithmeticFull.lean 13 declarations
- BiquadraticBasis.lean 30 declarations
- BiquadraticBasisGroupTransport.lean 7 declarations
- BiquadraticGoodPrimeUnramified.lean 1 declarations
- BiquadraticGoodPrimeUnramifiedSameWitnessEquiv.lean 1 declarations
- BiquadraticThetaMap.lean 3 declarations
- BoundedConductor.lean 1 declarations
- CharacterDeterminant.lean 3 declarations
- CharacterFrobenius.lean 7 declarations
- CharacterGlobalGreedyDeterminantFullLocalBounds.lean 1 declarations
- CharacterGlobalGreedyDeterminantMasterBounds.lean 1 declarations
- CharacterLegendre.lean 21 declarations
- CharacterMaster.lean 19 declarations
- ConditionalPrimeBias.lean 15 declarations
- ConductorCompletedL.lean 36 declarations
- DirichletRealZeroBound.lean 1 declarations
- DirichletRealZeroBoundProof.lean 1 declarations
- ExceptionalConductor.lean 8 declarations
- FrobeniusRetainedCharacterField.lean 1 declarations
- GaussSquarefreeBridge.lean 7 declarations
- IntegerCharacter.lean 27 declarations
- MangoldtMass.lean 4 declarations
- NormLogDerivLFunctionNegLogDerivZeta.lean 7 declarations
- PrimePowerTail.lean 8 declarations
- PrimeTerms.lean 5 declarations
- QuadraticGroupCharacterFrobenius.lean 1 declarations
- RealLogDerivConductorCompletedLDivisorTsum.lean 29 declarations
- SquarefreeRadicands.lean 5 declarations
- SumCharacterPeriodZero.lean 34 declarations
- UnconditionalPrimeBias.lean 5 declarations