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