RamificationTheory.HilbertRamification.DiscreteValuationRing.tameOrder_dvd_ord_of_fixed
The actual tame order divides the native length-based order of every actual nonzero fixed coefficient. The DVR valuation dictionary is confined to this one-ring owner.
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_dvd_ord_of_fixed
(R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
(G : Type v) [Group G] [Finite G] [MulSemiringAction G R]
(x : R) (hx : x ≠ 0) (hfixed : ∀ g : G, g • x = x) :
tameOrder R G ∣ (Ring.ord R x).toNat