Faithful.lean
Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.Faithful
0 declarations indexed from sourceView source ↗
Module documentation
Compatibility import for the shared ProCGroups results
The general group-theoretic definitions and proofs are maintained in ProCGroups.FiniteStepSolvableQuotients.Faithful. This module preserves existing downstream imports without duplicate declarations.
Imported by15
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.All
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.EmbeddingFormulation
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.FiniteFieldExtensions
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.PrimeOrderTest
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaAllPrimes
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaMaximalQuotient
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaOrdinary
- Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaProGroup
- Nyll.Yamaguchi26AbfaithfulGalois.HigherLocalField.Properties
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.CompletionComparison
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.Concrete.ResidueZeroUnramifiedFaithfulness
- Nyll.Yamaguchi26AbfaithfulGalois.Kummer.ResidueZeroFiniteRoots
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem4Dot1ResidueZeroLift
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem6Dot1FormalHilbert90
- Nyll.Yamaguchi26AbfaithfulGalois.Theorem6Dot5GroupCriterion
This module has no indexed declarations. Its imports and full source are available here.