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) : Invertible ↑t

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

Equations

• invertibleOfRingCharNotDvd not_dvd = invertibleOfNonzero (_ : ↑t = 0 → False)

theorem not_ringChar_dvd_of_invertible {K : Type u_1} [Field K] {t : ℕ} [Invertible ↑t] : ¬ringChar K ∣ t

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

• invertibleOfCharPNotDvd not_dvd = invertibleOfNonzero (_ : ↑t = 0 → False)

instance invertibleOfPos {K : Type u_1} [Field K] [CharZero K] (n : ℕ) [NeZero n] : Invertible ↑n

Equations

• invertibleOfPos n = invertibleOfNonzero (_ : ↑n ≠ 0)

instance invertibleSucc {K : Type u_1} [DivisionRing K] [CharZero K] (n : ℕ) : Invertible ↑(Nat.succ n)

Equations

• invertibleSucc n = invertibleOfNonzero (_ : ↑(Nat.succ n) ≠ 0)

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] : Invertible 2

Equations

• invertibleTwo = invertibleOfNonzero (_ : ↑2 ≠ 0)

instance invertibleThree {K : Type u_1} [DivisionRing K] [CharZero K] : Invertible 3

Equations

• invertibleThree = invertibleOfNonzero (_ : ↑3 ≠ 0)