class Lean.Grind.Field (α : Type u) extends Lean.Grind.CommRing α, Inv α, Div α : Type u

A field is a commutative ring with inverses for all non-zero elements.

• add : α → α → α
• mul : α → α → α
• hPow : α → Nat → α
• natCast : NatCast α
• ofNat (n : Nat) : OfNat α n
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• add_comm (a b : α) : a + b = b + a
• add_zero (a : α) : a + 0 = a
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• mul_one (a : α) : a * 1 = a
• one_mul (a : α) : 1 * a = a
• left_distrib (a b c : α) : a * (b + c) = a * b + a * c
• right_distrib (a b c : α) : (a + b) * c = a * c + b * c
• zero_mul (a : α) : 0 * a = 0
• mul_zero (a : α) : a * 0 = 0
• pow_zero (a : α) : a ^ 0 = 1
• pow_succ (a : α) (n : Nat) : a ^ (n + 1) = a ^ n * a
• ofNat_succ (a : Nat) : OfNat.ofNat (a + 1) = OfNat.ofNat a + 1
• ofNat_eq_natCast (n : Nat) : OfNat.ofNat n = ↑n
• neg : α → α
• sub : α → α → α
• intCast : IntCast α
• neg_add_cancel (a : α) : -a + a = 0
• sub_eq_add_neg (a b : α) : a - b = a + -b
• intCast_ofNat (n : Nat) : ↑(OfNat.ofNat n) = OfNat.ofNat n
• intCast_neg (i : Int) : ↑(-i) = -↑i
• mul_comm (a b : α) : a * b = b * a
• inv : α → α
• div : α → α → α
• div_eq_mul_inv (a b : α) : a / b = a * b⁻¹

  Division is multiplication by the inverse.

• zero_ne_one : 0 ≠ 1

  Zero is not equal to one: fields are non trivial.

• inv_zero : 0⁻¹ = 0

  The inverse of zero is zero. This is a "junk value" convention.

• mul_inv_cancel {a : α} : a ≠ 0 → a * a⁻¹ = 1

  The inverse of a non-zero element is a right inverse.

theorem Lean.Grind.Field.inv_mul_cancel {α : Type u_1} [Field α] {a : α} (h : a ≠ 0) : a⁻¹ * a = 1

theorem Lean.Grind.Field.eq_inv_of_mul_eq_one {α : Type u_1} [Field α] {a b : α} (h : a * b = 1) : a = b⁻¹

theorem Lean.Grind.Field.inv_one {α : Type u_1} [Field α] : 1⁻¹ = 1

theorem Lean.Grind.Field.inv_inv {α : Type u_1} [Field α] (a : α) : a⁻¹⁻¹ = a

theorem Lean.Grind.Field.inv_neg {α : Type u_1} [Field α] (a : α) : (-a)⁻¹ = -a⁻¹

theorem Lean.Grind.Field.inv_eq_zero_iff {α : Type u_1} [Field α] {a : α} : a⁻¹ = 0 ↔ a = 0

theorem Lean.Grind.Field.zero_eq_inv_iff {α : Type u_1} [Field α] {a : α} : 0 = a⁻¹ ↔ 0 = a

instance Lean.Grind.Field.instNoNatZeroDivisorsOfIsCharPOfNatNat {α : Type u_1} [Field α] [IsCharP α 0] : NoNatZeroDivisors α