HepLean 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
def invertibleOfRingCharNotDvd {K : Type u_1} [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_1} [Field K] {t : ℕ} [Invertible ↑t] :
    ¬ringChar K ∣ t
    source
    def invertibleOfCharPNotDvd {K : Type u_1} [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_1} [Field K] [CharZero K] (n : ℕ) [NeZero n] :
      Invertible ↑n
      Equations
      source
      instance invertibleSucc {K : Type u_1} [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_1} [DivisionRing K] [CharZero K] :
      Invertible 2
      Equations
      source
      instance invertibleThree {K : Type u_1} [DivisionRing K] [CharZero K] :
      Invertible 3
      Equations