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 : α → α → α
• natCast : NatCast α
• ofNat (n : Nat) : OfNat α n
• nsmul : SMul Nat α
• npow : HPow α Nat α
• add_zero (a : α) : a + 0 = a
• add_comm (a b : α) : a + b = b + a
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• 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
• nsmul_eq_natCast_mul (n : Nat) (a : α) : n • a = ↑n * a
• neg : α → α
• sub : α → α → α
• intCast : IntCast α
• zsmul : SMul Int α
• neg_add_cancel (a : α) : -a + a = 0
• sub_eq_add_neg (a b : α) : a - b = a + -b
• neg_zsmul (i : Int) (a : α) : -i • a = -(i • a)
• zsmul_natCast_eq_nsmul (n : Nat) (a : α) : ↑n • a = n • a
• 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 : α → α → α
• zpow : HPow α Int α

  An exponentiation operator.

• 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.

• zpow_zero (a : α) : a ^ 0 = 1

  The zeroth power of any element is one.

• zpow_succ (a : α) (n : Nat) : a ^ (↑n + 1) = a ^ ↑n * a

  The (n+1)-st power of any element is the element multiplied by the n-th power.

• zpow_neg (a : α) (n : Int) : a ^ (-n) = (a ^ n)⁻¹

  Raising to a negative power is the inverse of raising to the positive power.

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_eq_iff_eq_iff {α : Type u_1} [Field α] (a b : α) : a⁻¹ = b ↔ a = b⁻¹

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

theorem Lean.Grind.Field.of_mul_eq_zero {α : Type u_1} [Field α] {a b : α} : a * b = 0 → a = 0 ∨ b = 0

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

theorem Lean.Grind.Field.of_pow_eq_zero {α : Type u_1} [Field α] (a : α) (n : Nat) : a ^ n = 0 → a = 0

theorem Lean.Grind.Field.zpow_natCast {α : Type u_1} [Field α] (a : α) (n : Nat) : a ^ ↑n = a ^ n

theorem Lean.Grind.Field.zpow_one {α : Type u_1} [Field α] (a : α) : a ^ 1 = a

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

theorem Lean.Grind.Field.zpow_add_one {α : Type u_1} [Field α] {a : α} (h : a ≠ 0) (n : Int) : a ^ (n + 1) = a ^ n * a

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

theorem Lean.Grind.Field.zpow_add {α : Type u_1} [Field α] {a : α} (h : a ≠ 0) (m n : Int) : a ^ (m + n) = a ^ m * a ^ n

theorem Lean.Grind.Field.div_zero {α : Type u_1} [Field α] {x : α} : x / 0 = 0

theorem Lean.Grind.Field.mul_div {α : Type u_1} [Field α] {x y z : α} : x * (y / z) = x * y / z

theorem Lean.Grind.Field.div_mul {α : Type u_1} [Field α] {x y z : α} : x / y * z = x * z / y

theorem Lean.Grind.Field.div_add {α : Type u_1} [Field α] {x y z : α} (hy : y ≠ 0) : x / y + z = (x + y * z) / y

theorem Lean.Grind.Field.add_div {α : Type u_1} [Field α] {x y z : α} (hz : z ≠ 0) : x + y / z = (x * z + y) / z

theorem Lean.Grind.Field.div_div_right {α : Type u_1} [Field α] {x y z : α} : x / (y / z) = x * z / y

theorem Lean.Grind.Field.div_div_left {α : Type u_1} [Field α] {x y z : α} : x / y / z = x / (y * z)

theorem Lean.Grind.Field.div_mul_cancel {α : Type u_1} [Field α] {x y : α} (h : y ≠ 0) : x / y * y = x

theorem Lean.Grind.Field.natCast_ne_zero {α : Type u_1} [Field α] [IsCharP α 0] {n : Nat} (h : n ≠ 0) : ↑n ≠ 0

theorem Lean.Grind.Field.intCast_div_of_dvd {α : Type u_1} [Field α] {x y : Int} (h : y ∣ x) (w : ↑y ≠ 0) : ↑(x / y) = ↑x / ↑y

theorem Lean.Grind.Field.natCast_div_of_dvd {α : Type u_1} [Field α] {x y : Nat} (h : y ∣ x) (w : ↑y ≠ 0) : ↑(x / y) = ↑x / ↑y

def Lean.Grind.Field.noNatZeroDivisors.ofIsCharPZero {α : Type u_1} [Field α] [IsCharP α 0] : NoNatZeroDivisors α

Equations

• ⋯ = ⋯