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.

def invertibleOfRingCharNotDvd {K : Type u_1} [Field K] {t : } (not_dvd : ¬ringChar K t) :

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

Equations
Instances For
    def invertibleOfCharPNotDvd {K : Type u_1} [Field K] {p : } [CharP K p] {t : } (not_dvd : ¬p t) :

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

    Equations
    Instances For
      instance invertibleOfPos {K : Type u_1} [Field K] [CharZero K] (n : ) [NeZero n] :
      Equations
      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.

      instance invertibleTwo {K : Type u_1} [DivisionRing K] [CharZero K] :
      Equations
      instance invertibleThree {K : Type u_1} [DivisionRing K] [CharZero K] :
      Equations