RamificationTheory.HilbertRamification.DiscreteValuationRing.uniformizerRatioUnit_exists_coefficient
The actual ratio unit supplies an ordinary local coefficient, its unit proof, and its literal value. Unit coercions remain in this sparse local owner.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u vLean source · statement
theorem uniformizerRatioUnit_exists_coefficient
(R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
(G : Type v) [Group G] [MulSemiringAction G R]
(π : R) (hπ : Irreducible π) (g : G) :
∃ c : R, IsUnit c ∧
π * c = (MulSemiringAction.toRingHom G R g).toFun π ∧
c = (uniformizerRatioUnit R G π hπ g).val