LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exp_threshold_natCast_sq_mul
Every nonzero element of p² times the valuation ring lies strictly above the ramified exponential threshold.
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 exp_threshold_natCast_sq_mul
(v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
(p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
(a : v.valuationSubring) (hx : (p : K) ^ 2 * (a : K) ≠ 0) :
(v.residueRamificationIndex p : ℝ) / ((p : ℝ) - 1) <
((ofWithZeroValuation v).val (Units.mk0 ((p : K) ^ 2 * (a : K)) hx) : ℝ)