Documentation

Init.Grind.CommRing.Field

class Lean.Grind.Field (α : Type u) extends Lean.Grind.CommRing α, Inv α, Div α :
Instances
    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 : α) :
    theorem Lean.Grind.Field.inv_neg {α : Type u_1} [Field α] (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