RamificationTheory.HilbertRamification.DiscreteValuationRing.tameOrder_eq_card_quotient_principalUnitInertia
The actual tame image order is the cardinality of inertia modulo the same principal-unit subgroup, by the first isomorphism theorem.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u vLean source · statement
theorem tameOrder_eq_card_quotient_principalUnitInertia
(R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
(G : Type v) [Group G] [MulSemiringAction G R] :
tameOrder R G = Nat.card
((IsLocalRing.maximalIdeal R).inertia G ⧸ principalUnitInertia R G)