Module

Coprimality.lean

Nyll.EtaleFundamentalGroups.Inertia.Residue.Coprimality

1 declaration indexed from sourceView source ↗

Module documentation

Coprimality detected in a residue ring

The one-point inertia argument ends by mapping a ramification index to a residue ring of characteristic p. If that image is a unit, the index is prime to p. This file records that arithmetic endpoint without mentioning ramification or inertia.

Imports2

Mathlib.Algebra.CharP.Defs
Mathlib.Data.Nat.Prime.Defs

Imported by4

theorem

natCoprime_of_isUnit_natCast_of_charP

L23 ↗

EtaleFundamentalGroups.natCoprime_of_isUnit_natCast_of_charP

Documentation

A natural number that is invertible in a nontrivial ring of prime characteristic p is coprime to p.

Source context 1 command

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

namespace EtaleFundamentalGroups

Lean source · statement

theorem natCoprime_of_isUnit_natCast_of_charP
    {k : Type*} [CommRing k] [Nontrivial k]
    (p n : ℕ) [CharP k p] (hp : p.Prime)
    (hn : IsUnit (n : k)) : Nat.Coprime n p

Module documentation

Coprimality detected in a residue ring

Declarations

natCoprime_of_isUnit_natCast_of_charP