Module

LocalRingResidueCharacteristicTransport.lean

Nyll.SchemeTheory.RingTheory.Ramification.LocalRingResidueCharacteristicTransport

2 declarations indexed from sourceView source ↗

Module documentation

Residue characteristic under local-ring equivalences

Transports CharP and characteristic-zero instances between residue fields of isomorphic local rings.

Imports2

Mathlib.RingTheory.LocalRing.ResidueField.Basic
Mathlib.Algebra.CharP.Algebra

Imported by2

theorem

residueField_charP_of_ringEquiv

L21 ↗

SchemeTheory.residueField_charP_of_ringEquiv

Source context 2 commands

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

namespace SchemeTheory
universe u v

Lean source · statement

theorem residueField_charP_of_ringEquiv
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S]
    (e : R ≃+* S) (p : ℕ) [CharP (IsLocalRing.ResidueField R) p] :
    CharP (IsLocalRing.ResidueField S) p

theorem

residueField_charZero_of_ringEquiv

L30 ↗

SchemeTheory.residueField_charZero_of_ringEquiv