Module

BoundedCyclotomicCoefficient.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.BoundedCyclotomicCoefficient

1 declaration indexed from sourceView source ↗

Module documentation

Strict growth from a bounded cyclotomic coefficient

In mixed characteristic, a bounded exponent different from one gives a coefficient (1-a)/p^(s+1) of value strictly greater than one. The numerator has smaller p-adic order than the denominator. No completeness, discreteness, or finite residue-field hypothesis is used.

Imports3

Imported by2

theorem

one_lt_boundedCyclotomicCoefficient

L28 ↗

Valuation.one_lt_boundedCyclotomicCoefficient

Documentation

A nontrivial bounded cyclotomic exponent gives a coefficient whose multiplicative value is strictly greater than one.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace Valuation
universe u
variable {K : Type u} [Field K] [CharZero K]

Lean source · statement

theorem one_lt_boundedCyclotomicCoefficient
    (v : Valuation K (WithZero (Multiplicative ℤ))) (p a s : ℕ)
    [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
    (ha : a < p ^ (s + 1)) (ha1 : a ≠ 1) :
    1 < v ((1 - (a : K)) / (p : K) ^ (s + 1))

Module documentation

Strict growth from a bounded cyclotomic coefficient

Declarations

one_lt_boundedCyclotomicCoefficient