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.

@[simp]

theorem Even.all {R : Type u_1} [Semiring R] [Invertible 2] (a : R) : Even a

When two is invertible, every element is Even.

@[simp]

theorem Odd.all {R : Type u_1} [Ring R] [Invertible 2] (a : R) : Odd a

When two is invertible in a ring, every element is Odd.

theorem not_ringChar_dvd_of_invertible {R : Type u_1} [Ring R] {t : ℕ} [Invertible ↑t] [Nontrivial R] : ¬ringChar R ∣ t

theorem CharP.intCast_mul_natCast_gcdA_eq_gcd {R : Type u_1} [Ring R] {p : ℕ} [CharP R p] (n : ℕ) : ↑n * ↑(n.gcdA p) = ↑(n.gcd p)

theorem CharP.natCast_gcdA_mul_intCast_eq_gcd {R : Type u_1} [Ring R] {p : ℕ} [CharP R p] (n : ℕ) : ↑(n.gcdA p) * ↑n = ↑(n.gcd p)

def invertibleOfCoprime {R : Type u_1} [Ring R] {p : ℕ} [CharP R p] {n : ℕ} (h : n.Coprime p) : Invertible ↑n

In a ring of characteristic p, (n : R) is invertible when n is coprime with p, with inverse n.gcdA p.

theorem invOf_eq_of_coprime {R : Type u_1} [Ring R] {p : ℕ} [CharP R p] {n : ℕ} [Invertible ↑n] (h : n.Coprime p) : ⅟↑n = ↑(n.gcdA p)

theorem CharP.isUnit_natCast_iff {R : Type u_1} [Ring R] {p : ℕ} [CharP R p] {n : ℕ} (hp : Nat.Prime p) : IsUnit ↑n ↔ ¬p ∣ n

theorem CharP.isUnit_ofNat_iff {R : Type u_1} [Ring R] {p : ℕ} [CharP R p] {n : ℕ} [n.AtLeastTwo] (hp : Nat.Prime p) : IsUnit (OfNat.ofNat n) ↔ ¬p ∣ OfNat.ofNat n

theorem CharP.isUnit_intCast_iff {R : Type u_1} [Ring R] {p : ℕ} [CharP R p] {z : ℤ} (hp : Nat.Prime p) : IsUnit ↑z ↔ ¬↑p ∣ z

def invertibleOfRingCharNotDvd {K : Type u_2} [Semifield K] {t : ℕ} (not_dvd : ¬ringChar K ∣ t) : Invertible ↑t

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

def invertibleOfCharPNotDvd {K : Type u_2} [Semifield K] {p : ℕ} [CharP K p] {t : ℕ} (not_dvd : ¬p ∣ t) : Invertible ↑t

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

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

instance invertibleSucc {K : Type u_2} [DivisionSemiring K] [CharZero K] (n : ℕ) : Invertible ↑n.succ

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_2} [DivisionSemiring K] [CharZero K] : Invertible 2

instance invertibleThree {K : Type u_2} [DivisionSemiring K] [CharZero K] : Invertible 3