Module

PrincipalUnitTorsion.lean

Nyll.ValuedFieldTheory.Valuation.PrincipalUnitTorsion

1 declaration indexed from sourceView source ↗

Module documentation

Prime-to-residue torsion in the actual principal-unit group

For a principal unit x, reduction of the geometric sum of its first n powers is n. If n is nonzero in the residue field, this sum is nonzero. The geometric-sum identity then makes x^n = 1 imply x = 1. No Henselianity, discreteness, completeness, or characteristic assumption on the field is used.

Imports2

Mathlib.RingTheory.Valuation.ValuationSubring
Mathlib.Algebra.Ring.GeomSum

Imported by2

theorem

principalUnit_eq_one_of_pow_eq_one_of_residue_natCast_ne_zero

L28 ↗

ValuationSubring.principalUnit_eq_one_of_pow_eq_one_of_residue_natCast_ne_zero

Documentation

A principal unit killed by an integer nonzero in the residue field is one.

Source context 4 commands

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

namespace ValuationSubring
open scoped BigOperators
universe u
variable {K : Type u} [Field K]

Lean source · statement

theorem principalUnit_eq_one_of_pow_eq_one_of_residue_natCast_ne_zero
    (A : ValuationSubring K) (x : A.principalUnitGroup)
    (n : ℕ) (hn : (n : IsLocalRing.ResidueField A) ≠ 0)
    (hx : x ^ n = 1) : x = 1

Module documentation

Prime-to-residue torsion in the actual principal-unit group

Declarations

principalUnit_eq_one_of_pow_eq_one_of_residue_natCast_ne_zero