All.lean
Nyll.Yamaguchi26AbfaithfulGalois.All
0 declarations indexed from sourceView source ↗
Module documentation
Ab-faithfulness of absolute Galois groups
Formalization of Naganori Yamaguchi's Ab-faithfulness of absolute Galois groups in number theory, using the numbering of arXiv v1. Covers solvable extensions, cohomological criteria, slimness and field examples. Example 2.2, Lemma 6.8 and the general Hilbertian application remain outside the formalization.
Imports26
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem1Dot1AbFaithfulness
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem1Dot2PrimeOrderTest
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem1Dot3SigmaProperties
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem2Dot1ElementarySplitCriterion
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem3Dot1PrimePowerRoots
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem3Dot3FiniteOrderModP
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem3Dot4PrincipalUnitLogarithm
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem3Dot5CompletePrimeDegree
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem3Dot6MixedCharacteristic
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem4Dot1ResidueZeroLift
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem4Dot2HigherLocalFields
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem5Dot1FaithfulAbelianExtension
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem5Dot2AbelianSplitSolvableSlim
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem6Dot1FormalHilbert90
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem6Dot2IntegralInvariants
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem6Dot3CentralizerCriterion
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem6Dot4RelativeCriterion
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem6Dot5GroupCriterion
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem6Dot6AbsoluteCenter
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem6Dot7FieldSlimExamples
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.All
- Nyll.Yamaguchi26AbfaithfulGalois.HigherLocalField.All
- Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.All
- Nyll.Yamaguchi26AbfaithfulGalois.FieldExamples.All
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.All
- Nyll.Yamaguchi26AbfaithfulGalois.Analytic.All
Imported by1
This module has no indexed declarations. Its imports and full source are available here.