Documentation

Mathlib.Algebra.CharP.Invertible

Invertibility of elements given a characteristic #

This file includes some instances of Invertible for specific numbers in characteristic zero. Some more cases are given as a def, to be included only when needed. To construct instances for concrete numbers, invertibleOfNonzero is a useful definition.

source
theorem CharP.intCast_mul_natCast_gcdA_eq_gcd {R : Type u_1} [Ring R] {p : ℕ} [CharP R p] (n : ℕ) :
↑n * ↑(n.gcdA p) = ↑(n.gcd p)
source
theorem CharP.natCast_gcdA_mul_intCast_eq_gcd {R : Type u_1} [Ring R] {p : ℕ} [CharP R p] (n : ℕ) :
↑(n.gcdA p) * ↑n = ↑(n.gcd p)
source
def invertibleOfCoprime {R : Type u_1} [Ring R] {p : ℕ} [CharP R p] {n : ℕ} (h : n.Coprime p) :
Invertible ↑n

In a ring of characteristic p, (n : R) is invertible when n is coprime with p, with inverse n.gcdA p.

Equations
Instances For
    source
    theorem invOf_eq_of_coprime {R : Type u_1} [Ring R] {p : ℕ} [CharP R p] {n : ℕ} [Invertible ↑n] (h : n.Coprime p) :
    ⅟ ↑n = ↑(n.gcdA p)
    source
    theorem CharP.isUnit_natCast_iff {R : Type u_1} [Ring R] {p : ℕ} [CharP R p] {n : ℕ} (hp : Nat.Prime p) :
    IsUnit ↑n ↔ ¬p ∣ n
    source
    theorem CharP.isUnit_ofNat_iff {R : Type u_1} [Ring R] {p : ℕ} [CharP R p] {n : ℕ} [n.AtLeastTwo] (hp : Nat.Prime p) :
    IsUnit (OfNat.ofNat n) ↔ ¬p ∣ OfNat.ofNat n
    source
    theorem CharP.isUnit_intCast_iff {R : Type u_1} [Ring R] {p : ℕ} [CharP R p] {z : ℤ} (hp : Nat.Prime p) :
    IsUnit ↑z ↔ ¬↑p ∣ z
    source
    def invertibleOfRingCharNotDvd {K : Type u_2} [Field K] {t : ℕ} (not_dvd : ¬ringChar K ∣ t) :
    Invertible ↑t

    A natural number t is invertible in a field K if the characteristic of K does not divide t.

    Equations
    Instances For
      source
      theorem not_ringChar_dvd_of_invertible {K : Type u_2} [Field K] {t : ℕ} [Invertible ↑t] :
      ¬ringChar K ∣ t
      source
      def invertibleOfCharPNotDvd {K : Type u_2} [Field K] {p : ℕ} [CharP K p] {t : ℕ} (not_dvd : ¬p ∣ t) :
      Invertible ↑t

      A natural number t is invertible in a field K of characteristic p if p does not divide t.

      Equations
      Instances For
        source
        instance invertibleOfPos {K : Type u_2} [Field K] [CharZero K] (n : ℕ) [NeZero n] :
        Invertible ↑n
        Equations
        source
        instance invertibleSucc {K : Type u_2} [DivisionRing K] [CharZero K] (n : ℕ) :
        Invertible ↑n.succ
        Equations

        A few Invertible n instances for small numerals n. Feel free to add your own number when you need its inverse.

        source
        instance invertibleTwo {K : Type u_2} [DivisionRing K] [CharZero K] :
        Invertible 2
        Equations
        source
        instance invertibleThree {K : Type u_2} [DivisionRing K] [CharZero K] :
        Invertible 3
        Equations