ModuleTameOrderDivisibility.lean
Nyll.EtaleFundamentalGroups.Inertia.TameOrderDivisibility
2 declarations indexed from sourceView source ↗ Module documentation
Prime-to-characteristic divisors survive the wild quotient
The order of a finite p-group divides a power of p. Thus every divisor of the inertia order coprime to p divides the index of wild inertia. This converts the actual radical ramification divisibility into finite tame-order divisibility once the finite inertia cardinality has been supplied.
Imports3
- Mathlib.Algebra.CharP.Invertible
- Mathlib.GroupTheory.Coset.Card
- Mathlib.GroupTheory.PGroup
Imported by3
Declarations
EtaleFundamentalGroups.Inertia.natCast_isUnit_coprime_ringExpChar
DocumentationInvertibility of an actual residue-field integer makes it coprime to that field's own exponential characteristic, including characteristic zero.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
universe u
EtaleFundamentalGroups.Inertia.primeTo_dvd_quotient_card_of_dvd_card_of_isPGroup
DocumentationA divisor prime to p survives quotienting a finite group by any p-subgroup. Normality is not needed for the index calculation.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
universe u