mathlib documentation

algebra.char_p.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, invertible_of_nonzero is a useful definition.

def invertible_of_ring_char_not_dvd {K : Type u_1} [field K] {t : } (not_dvd : ¬ring_char K t) :

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

Equations
theorem not_ring_char_dvd_of_invertible {K : Type u_1} [field K] {t : } [invertible t] :
def invertible_of_char_p_not_dvd {K : Type u_1} [field K] {p : } [char_p K p] {t : } (not_dvd : ¬p t) :

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

Equations
@[instance]
def invertible_of_pos {K : Type u_1} [field K] [char_zero K] (n : ) [h : fact (0 < n)] :
Equations
@[instance]
def invertible_succ {K : Type u_1} [division_ring K] [char_zero K] (n : ) :
Equations

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

@[instance]
def invertible_two {K : Type u_1} [division_ring K] [char_zero K] :
Equations
@[instance]
def invertible_three {K : Type u_1} [division_ring K] [char_zero K] :
Equations