Module

ComapResidueCharP.lean

Nyll.ValuedFieldTheory.Valuation.ComapResidueCharP

1 declaration indexed from sourceView source ↗

Module documentation

Residue characteristic under pullback of valuations

The residue-field characteristic of a valuation subring is preserved by pullback along a field embedding. The proof compares natural-number casts with membership in the nonunits.

Imports2

Nyll.ValuedFieldTheory.Valuation.ComapResidueCharacteristic
Mathlib.Algebra.CharP.Defs

Imported by4

theorem

charP_residueField_comap

L24 ↗

ValuationSubring.charP_residueField_comap

Documentation

The residue characteristic of the specified valuation subring is preserved by pullback along any field embedding.

Source context 2 commands

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

namespace ValuationSubring
universe u v

Lean source · statement

theorem charP_residueField_comap
    {K : Type u} {L : Type v} [Field K] [Field L]
    (A : ValuationSubring L) (f : K →+* L) (p : ℕ)
    [CharP (IsLocalRing.ResidueField A) p] :
    CharP (IsLocalRing.ResidueField (A.comap f)) p

Module documentation

Residue characteristic under pullback of valuations

Declarations

charP_residueField_comap