All.lean
Nyll.Yamaguchi26AbfaithfulGalois.Analytic.All
0 declarations indexed from sourceView source ↗
Module documentation
Analytic principal-unit methods
This aggregate collects principal-unit logarithms and exponentials, cyclotomic eigenunits, and logarithmic character methods used in the abelian-faithfulness results.
Imports12
- Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitLog
- Nyll.Yamaguchi26AbfaithfulGalois.Analytic.PrincipalUnitExpLog
- Nyll.Yamaguchi26AbfaithfulGalois.Analytic.LogImageProperties
- Nyll.Yamaguchi26AbfaithfulGalois.Analytic.MixedCharCharacterLogImage
- Nyll.Yamaguchi26AbfaithfulGalois.Analytic.MixedCharCharacterLogMinimum
- Nyll.Yamaguchi26AbfaithfulGalois.Analytic.MixedCharCharacterLogRepresentation
- Nyll.Yamaguchi26AbfaithfulGalois.Analytic.MixedCharCharacterLogRigidity
- Nyll.Yamaguchi26AbfaithfulGalois.Analytic.MixedCharCyclotomicEigenUnit
- Nyll.Yamaguchi26AbfaithfulGalois.Analytic.MixedCharPrincipalUnitEigenLift
- Nyll.Yamaguchi26AbfaithfulGalois.Analytic.MixedCharPrincipalUnitPowerWitnessDecrease
- Nyll.Yamaguchi26AbfaithfulGalois.Analytic.MixedCharPrincipalUnitPowerWitnessLog
- Nyll.Yamaguchi26AbfaithfulGalois.Analytic.MixedCharSubgroupCharacterLogVector
Imported by1
This module has no indexed declarations. Its imports and full source are available here.