Module

PrincipalUnitRoots.lean

Nyll.ValuedFieldTheory.Valuation.PrincipalUnitRoots

1 declaration indexed from sourceView source ↗

Module documentation

Prime-power roots of principal units

In residue characteristic p, if a p-power of a field element is a principal unit, so is the element. This uses neither discreteness nor completeness of the valuation, and does not require the residue field to be perfect.

Imports3

Mathlib.Algebra.CharP.Reduced
Mathlib.Algebra.Order.GroupWithZero.Canonical
Mathlib.RingTheory.Valuation.ValuationSubring

Imported by2

theorem

map_eq_one_and_sub_one_lt_one_of_prime_pow

L26 ↗

Valuation.map_eq_one_and_sub_one_lt_one_of_prime_pow

Documentation

A prime-power root of a principal unit is itself a principal unit, for an arbitrary ordered value group.

Source context 2 commands

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

namespace Valuation
universe u v

Lean source · statement

theorem map_eq_one_and_sub_one_lt_one_of_prime_pow
    {K : Type u} {Γ : Type v} [Field K] [LinearOrderedCommGroupWithZero Γ]
    (v : Valuation K Γ)
    (p : ℕ) [Fact p.Prime]
    [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
    (s : ℕ) (y : K) (hy : v (y ^ (p ^ s) - 1) < 1) :
    v y = 1 ∧ v (y - 1) < 1

Module documentation

Prime-power roots of principal units

Declarations

map_eq_one_and_sub_one_lt_one_of_prime_pow