Module

FiniteOrderAutomorphism.lean

Nyll.ValuedFieldTheory.Valuation.FiniteOrderAutomorphism

1 declaration indexed from sourceView source ↗

Module documentation

Finite-order automorphisms preserving a valuation class

An order-preserving permutation of a finite orbit cannot change the valuation value at any point. Thus finite-order automorphisms preserving a valuation class preserve the valuation itself.

Imports3

Mathlib.RingTheory.Valuation.Basic
Mathlib.Algebra.Ring.Aut
Mathlib.Order.Monotone.Basic

Imported by2

theorem

map_apply_eq_of_isEquiv_comap_of_pow_eq_one

L25 ↗

Valuation.map_apply_eq_of_isEquiv_comap_of_pow_eq_one

Documentation

A finite-order field automorphism preserving a valuation class preserves its actual values, without any discreteness hypothesis.

Source context 2 commands

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

namespace Valuation
variable {K Γ : Type*} [Field K] [LinearOrderedCommGroupWithZero Γ]

Lean source · statement

theorem map_apply_eq_of_isEquiv_comap_of_pow_eq_one
    (v : Valuation K Γ) (τ : K ≃+* K)
    (hτ : v.IsEquiv (v.comap τ.toRingHom))
    (n : ℕ) (hn : 0 < n) (hpow : τ ^ n = 1) (x : K) : v (τ x) = v x

Module documentation

Finite-order automorphisms preserving a valuation class

Declarations

map_apply_eq_of_isEquiv_comap_of_pow_eq_one