Documentation

LeanPool.CCDN.Algebra.CharZeroOrGT

Characteristic zero or larger than a bound #

CharZeroOrGT R n says that the positive natural numbers up to n are nonzero in R. For a field this means that the characteristic is zero or larger than n. Results that hold both in characteristic zero and in characteristic p > n are stated once under this hypothesis.

Main results #

source
def CCDN.CharZeroOrGT (R : Type u_1) [AddMonoidWithOne R] (n : ℕ) :
Prop

The positive natural numbers up to n are nonzero in R; for a field, the characteristic of R is zero or larger than n.

Equations
Instances For
    source
    theorem CCDN.CharZeroOrGT.of_charZero {R : Type u_1} [AddMonoidWithOne R] [CharZero R] (n : ℕ) :
    CharZeroOrGT R n

    Characteristic zero exceeds every bound.

    source
    theorem CCDN.CharZeroOrGT.of_charP {R : Type u_1} [AddMonoidWithOne R] {p n : ℕ} [CharP R p] (h : n < p) :
    CharZeroOrGT R n

    Characteristic p exceeds every bound below p.

    source
    theorem CCDN.CharZeroOrGT.mono {R : Type u_1} [AddMonoidWithOne R] {m n : ℕ} (h : CharZeroOrGT R n) (hmn : m ≤ n) :
    CharZeroOrGT R m

    The hypothesis weakens to any smaller bound.

    source
    theorem CCDN.CharZeroOrGT.natCast_ne_zero {R : Type u_1} [AddMonoidWithOne R] {m n : ℕ} (h : CharZeroOrGT R n) (hm : m ≠ 0) (hmn : m ≤ n) :
    ↑m ≠ 0

    A positive natural number up to the bound is nonzero.

    source
    theorem CCDN.CharZeroOrGT.map {R : Type u_1} {S : Type u_2} [DivisionRing R] [Semiring S] [Nontrivial S] {n : ℕ} (h : CharZeroOrGT R n) (φ : R →+* S) :
    CharZeroOrGT S n

    The hypothesis passes along a ring homomorphism out of a division ring, such as the algebra map of a field extension.

    source
    theorem CCDN.CharZeroOrGT.iff_ringChar {R : Type u_1} [NonAssocSemiring R] {n : ℕ} :
    CharZeroOrGT R n ↔ ringChar R = 0 ∨ n < ringChar R

    CharZeroOrGT R n says exactly that the characteristic of R is zero or exceeds n.