mathlib3 documentation

algebra.char_p.invertible

Invertibility of elements given a characteristic #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
def invertible_of_ring_char_not_dvd {K : Type u_1} [field K] {t : ℕ} (not_dvd : ¬ring_char K ∣ t) :
invertible ↑t

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

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

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

Equations
source
@[protected, instance]
def invertible_of_pos {K : Type u_1} [field K] [char_zero K] (n : ℕ) [ne_zero n] :
invertible ↑n
Equations
source
@[protected, instance]
def invertible_succ {K : Type u_1} [division_ring K] [char_zero 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
@[protected, instance]
def invertible_two {K : Type u_1} [division_ring K] [char_zero K] :
invertible 2
Equations
source
@[protected, instance]
def invertible_three {K : Type u_1} [division_ring K] [char_zero K] :
invertible 3
Equations