LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_principalUnitLog_denominator_min_bound
The exact denominator minimum bounds every nonzero logarithmic value.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u
variable {K : Type u} [Field K] [CharZero K]Lean source · statement
theorem exists_principalUnitLog_denominator_min_bound
(v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
[ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
(p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p] :
∃ m : ℕ,
(∀ n : ℕ,
((m + 1 : ℕ) : ℤ) - (v.residueRamificationIndex p : ℤ) *
(padicValNat p (m + 1) : ℤ) ≤
((n + 1 : ℕ) : ℤ) - (v.residueRamificationIndex p : ℤ) *
(padicValNat p (n + 1) : ℤ)) ∧
∀ u : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1,
∀ hu : (principalUnitLogOfMixedChar v p u).toAdd ≠ 0,
((m + 1 : ℕ) : ℤ) - (v.residueRamificationIndex p : ℤ) *
(padicValNat p (m + 1) : ℤ) ≤
(ofWithZeroValuation v).val
(Units.mk0 (principalUnitLogOfMixedChar v p u).toAdd hu)