# 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} [] {t : } (not_dvd : ¬ t) :

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

Instances For
theorem not_ringChar_dvd_of_invertible {K : Type u_1} [] {t : } [] :
def invertibleOfCharPNotDvd {K : Type u_1} [] {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.

Instances For
instance invertibleOfPos {K : Type u_1} [] [] (n : ) [] :
instance invertibleSucc {K : Type u_1} [] [] (n : ) :

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} [] [] :
instance invertibleThree {K : Type u_1} [] [] :