theorem Lean.Grind.Ring.OfSemiring.instAssociativeHAdd (α : Type u) [Semiring α] : Std.Associative fun (x1 x2 : α) => x1 + x2

theorem Lean.Grind.Ring.OfSemiring.instCommutativeHAdd (α : Type u) [Semiring α] : Std.Commutative fun (x1 x2 : α) => x1 + x2

theorem Lean.Grind.Ring.OfSemiring.instAssociativeHMul (α : Type u) [Semiring α] : Std.Associative fun (x1 x2 : α) => x1 * x2

def Lean.Grind.Ring.OfSemiring.r (α : Type u) [Semiring α] : α × α → α × α → Prop

Equations

• Lean.Grind.Ring.OfSemiring.r α (a, b) (c, d) = ∃ (k : α), a + d + k = b + c + k

@[implicit_reducible]

def Lean.Grind.Ring.OfSemiring.Q (α : Type u) [Semiring α] : Type u

Equations

• Lean.Grind.Ring.OfSemiring.Q α = Quot (Lean.Grind.Ring.OfSemiring.r α)

theorem Lean.Grind.Ring.OfSemiring.r_rfl {α : Type u} [Semiring α] (a : α × α) : r α a a

theorem Lean.Grind.Ring.OfSemiring.r_sym {α : Type u} [Semiring α] {a b : α × α} : r α a b → r α b a

theorem Lean.Grind.Ring.OfSemiring.r_trans {α : Type u} [Semiring α] {a b c : α × α} : r α a b → r α b c → r α a c

theorem Lean.Grind.Ring.OfSemiring.mul_helper {α : Type u_1} [Semiring α] {a₁ b₁ a₂ b₂ a₃ b₃ a₄ b₄ k₁ k₂ : α} (h₁ : a₁ + b₃ + k₁ = b₁ + a₃ + k₁) (h₂ : a₂ + b₄ + k₂ = b₂ + a₄ + k₂) : ∃ (k : α), a₁ * a₂ + b₁ * b₂ + (a₃ * b₄ + b₃ * a₄) + k = a₁ * b₂ + b₁ * a₂ + (a₃ * a₄ + b₃ * b₄) + k

def Lean.Grind.Ring.OfSemiring.Q.mk {α : Type u} [Semiring α] (p : α × α) : Q α

Equations

• Lean.Grind.Ring.OfSemiring.Q.mk p = Quot.mk (Lean.Grind.Ring.OfSemiring.r α) p

def Lean.Grind.Ring.OfSemiring.Q.liftOn₂ {α : Type u} [Semiring α] {β : Sort u_1} (q₁ q₂ : Q α) (f : α × α → α × α → β) (h : ∀ {a₁ b₁ a₂ b₂ : α × α}, r α a₁ a₂ → r α b₁ b₂ → f a₁ b₁ = f a₂ b₂) : β

Equations

• q₁.liftOn₂ q₂ f h = Quot.lift (fun (a₁ : α × α) => Quot.lift (f a₁) ⋯ q₂) ⋯ q₁

theorem Lean.Grind.Ring.OfSemiring.Q.ind {α : Type u} [Semiring α] {β : Q α → Prop} (mk : ∀ (a : α × α), β (mk a)) (q : Q α) : β q

def Lean.Grind.Ring.OfSemiring.natCast {α : Type u} [Semiring α] (n : Nat) : Q α

Equations

• Lean.Grind.Ring.OfSemiring.natCast n = Lean.Grind.Ring.OfSemiring.Q.mk (↑n, 0)

def Lean.Grind.Ring.OfSemiring.intCast {α : Type u} [Semiring α] (n : Int) : Q α

Equations

• Lean.Grind.Ring.OfSemiring.intCast n = if n < 0 then Lean.Grind.Ring.OfSemiring.Q.mk (0, ↑n.natAbs) else Lean.Grind.Ring.OfSemiring.Q.mk (↑n.natAbs, 0)

def Lean.Grind.Ring.OfSemiring.sub {α : Type u} [Semiring α] (q₁ q₂ : Q α) : Q α

Equations

• One or more equations did not get rendered due to their size.

def Lean.Grind.Ring.OfSemiring.add {α : Type u} [Semiring α] (q₁ q₂ : Q α) : Q α

Equations

• One or more equations did not get rendered due to their size.

def Lean.Grind.Ring.OfSemiring.mul {α : Type u} [Semiring α] (q₁ q₂ : Q α) : Q α

Equations

• One or more equations did not get rendered due to their size.

def Lean.Grind.Ring.OfSemiring.neg {α : Type u} [Semiring α] (q : Q α) : Q α

Equations

• Lean.Grind.Ring.OfSemiring.neg q = Quot.liftOn q (fun (x : α × α) => match x with | (a, b) => Lean.Grind.Ring.OfSemiring.Q.mk (b, a)) ⋯

theorem Lean.Grind.Ring.OfSemiring.neg_add_cancel {α : Type u} [Semiring α] (a : Q α) : add (neg a) a = natCast 0

theorem Lean.Grind.Ring.OfSemiring.add_comm {α : Type u} [Semiring α] (a b : Q α) : add a b = add b a

theorem Lean.Grind.Ring.OfSemiring.add_zero {α : Type u} [Semiring α] (a : Q α) : add a (natCast 0) = a

theorem Lean.Grind.Ring.OfSemiring.add_assoc {α : Type u} [Semiring α] (a b c : Q α) : add (add a b) c = add a (add b c)

theorem Lean.Grind.Ring.OfSemiring.sub_eq_add_neg {α : Type u} [Semiring α] (a b : Q α) : sub a b = add a (neg b)

theorem Lean.Grind.Ring.OfSemiring.intCast_neg {α : Type u} [Semiring α] (i : Int) : intCast (-i) = neg (intCast i)

theorem Lean.Grind.Ring.OfSemiring.intCast_ofNat {α : Type u} [Semiring α] (n : Nat) : intCast (OfNat.ofNat n) = natCast n

theorem Lean.Grind.Ring.OfSemiring.ofNat_succ {α : Type u} [Semiring α] (a : Nat) : natCast (a + 1) = add (natCast a) (natCast 1)

theorem Lean.Grind.Ring.OfSemiring.mul_assoc {α : Type u} [Semiring α] (a b c : Q α) : mul (mul a b) c = mul a (mul b c)

theorem Lean.Grind.Ring.OfSemiring.mul_one {α : Type u} [Semiring α] (a : Q α) : mul a (natCast 1) = a

theorem Lean.Grind.Ring.OfSemiring.one_mul {α : Type u} [Semiring α] (a : Q α) : mul (natCast 1) a = a

theorem Lean.Grind.Ring.OfSemiring.zero_mul {α : Type u} [Semiring α] (a : Q α) : mul (natCast 0) a = natCast 0

theorem Lean.Grind.Ring.OfSemiring.mul_zero {α : Type u} [Semiring α] (a : Q α) : mul a (natCast 0) = natCast 0

theorem Lean.Grind.Ring.OfSemiring.left_distrib {α : Type u} [Semiring α] (a b c : Q α) : mul a (add b c) = add (mul a b) (mul a c)

theorem Lean.Grind.Ring.OfSemiring.right_distrib {α : Type u} [Semiring α] (a b c : Q α) : mul (add a b) c = add (mul a c) (mul b c)

def Lean.Grind.Ring.OfSemiring.npow {α : Type u} [Semiring α] (a : Q α) (n : Nat) : Q α

Equations

• Lean.Grind.Ring.OfSemiring.npow a 0 = Lean.Grind.Ring.OfSemiring.natCast 1
• Lean.Grind.Ring.OfSemiring.npow a n_2.succ = Lean.Grind.Ring.OfSemiring.mul (Lean.Grind.Ring.OfSemiring.npow a n_2) a

theorem Lean.Grind.Ring.OfSemiring.pow_zero {α : Type u} [Semiring α] (a : Q α) : npow a 0 = natCast 1

theorem Lean.Grind.Ring.OfSemiring.pow_succ {α : Type u} [Semiring α] (a : Q α) (n : Nat) : npow a (n + 1) = mul (npow a n) a

def Lean.Grind.Ring.OfSemiring.nsmul {α : Type u} [Semiring α] (n : Nat) (a : Q α) : Q α

Equations

• Lean.Grind.Ring.OfSemiring.nsmul n a = Lean.Grind.Ring.OfSemiring.mul (Lean.Grind.Ring.OfSemiring.natCast n) a

def Lean.Grind.Ring.OfSemiring.zsmul {α : Type u} [Semiring α] (i : Int) (a : Q α) : Q α

Equations

• Lean.Grind.Ring.OfSemiring.zsmul i a = Lean.Grind.Ring.OfSemiring.mul (Lean.Grind.Ring.OfSemiring.intCast i) a

theorem Lean.Grind.Ring.OfSemiring.neg_zsmul {α : Type u} [Semiring α] (i : Int) (a : Q α) : zsmul (-i) a = neg (zsmul i a)

@[instance_reducible]

instance Lean.Grind.Ring.OfSemiring.ofSemiring {α : Type u} [Semiring α] : Ring (Q α)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Grind.Ring.OfSemiring.toQ {α : Type u} [Semiring α] (a : α) : Q α

Equations

• ↑a = Lean.Grind.Ring.OfSemiring.Q.mk (a, 0)

Embedding theorems

theorem Lean.Grind.Ring.OfSemiring.toQ_zero {α : Type u} [Semiring α] : ↑0 = 0

theorem Lean.Grind.Ring.OfSemiring.toQ_add {α : Type u} [Semiring α] (a b : α) : ↑(a + b) = ↑a + ↑b

theorem Lean.Grind.Ring.OfSemiring.toQ_mul {α : Type u} [Semiring α] (a b : α) : ↑(a * b) = ↑a * ↑b

theorem Lean.Grind.Ring.OfSemiring.toQ_natCast {α : Type u} [Semiring α] (n : Nat) : ↑(natCast n) = natCast n

theorem Lean.Grind.Ring.OfSemiring.toQ_ofNat {α : Type u} [Semiring α] (n : Nat) : ↑(OfNat.ofNat n) = OfNat.ofNat n

theorem Lean.Grind.Ring.OfSemiring.toQ_pow {α : Type u} [Semiring α] (a : α) (n : Nat) : ↑(a ^ n) = ↑a ^ n

Helper definitions and theorems for proving toQ is injective when CommSemiring has the right_cancel property

theorem Lean.Grind.Ring.OfSemiring.Q.exact {α : Type u} [Semiring α] {a b : α × α} : mk a = mk b → r α a b

theorem Lean.Grind.Ring.OfSemiring.toQ_inj {α : Type u} [Semiring α] [AddRightCancel α] {a b : α} : ↑a = ↑b → a = b

@[instance 10000]

instance Lean.Grind.Ring.OfSemiring.instNoNatZeroDivisorsQOfAddRightCancel {α : Type u} [Semiring α] [AddRightCancel α] [NoNatZeroDivisors α] : NoNatZeroDivisors (Q α)

@[instance 10000]

instance Lean.Grind.Ring.OfSemiring.instIsCharPQOfAddRightCancel {α : Type u} {p : Nat} [Semiring α] [AddRightCancel α] [IsCharP α p] : IsCharP (Q α) p

@[instance_reducible, instance 10000]

instance Lean.Grind.Ring.OfSemiring.instLEQOfOrderedAdd {α : Type u} [Semiring α] [LE α] [Std.IsPreorder α] [OrderedAdd α] : LE (Q α)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible, instance 10000]

instance Lean.Grind.Ring.OfSemiring.instLTQOfOrderedAdd {α : Type u} [Semiring α] [LE α] [Std.IsPreorder α] [OrderedAdd α] : LT (Q α)

Equations

• Lean.Grind.Ring.OfSemiring.instLTQOfOrderedAdd = { lt := fun (a b : Lean.Grind.Ring.OfSemiring.Q α) => a ≤ b ∧ ¬b ≤ a }

theorem Lean.Grind.Ring.OfSemiring.mk_le_mk {α : Type u} [Semiring α] [LE α] [Std.IsPreorder α] [OrderedAdd α] {a₁ a₂ b₁ b₂ : α} : Q.mk (a₁, a₂) ≤ Q.mk (b₁, b₂) ↔ a₁ + b₂ ≤ a₂ + b₁

@[instance 10000]

instance Lean.Grind.Ring.OfSemiring.instIsPreorderQ {α : Type u} [Semiring α] [LE α] [Std.IsPreorder α] [OrderedAdd α] : Std.IsPreorder (Q α)

theorem Lean.Grind.Ring.OfSemiring.toQ_le {α : Type u} [Semiring α] [LE α] [Std.IsPreorder α] [OrderedAdd α] {a b : α} : ↑a ≤ ↑b ↔ a ≤ b

theorem Lean.Grind.Ring.OfSemiring.toQ_lt {α : Type u} [Semiring α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedAdd α] {a b : α} : ↑a < ↑b ↔ a < b

@[instance 10000]

instance Lean.Grind.Ring.OfSemiring.instOrderedAddQ {α : Type u} [Semiring α] [LE α] [Std.IsPreorder α] [OrderedAdd α] : OrderedAdd (Q α)

@[instance 10000]

instance Lean.Grind.Ring.OfSemiring.instOrderedRingQOfLawfulOrderLTOfExistsAddOfLT {α : Type u} [Semiring α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedRing α] [ExistsAddOfLT α] : OrderedRing (Q α)

theorem Lean.Grind.CommRing.OfCommSemiring.instAssociativeHAdd (α : Type u) [CommSemiring α] : Std.Associative fun (x1 x2 : α) => x1 + x2

theorem Lean.Grind.CommRing.OfCommSemiring.instCommutativeHAdd (α : Type u) [CommSemiring α] : Std.Commutative fun (x1 x2 : α) => x1 + x2

theorem Lean.Grind.CommRing.OfCommSemiring.instAssociativeHMul (α : Type u) [CommSemiring α] : Std.Associative fun (x1 x2 : α) => x1 * x2

theorem Lean.Grind.CommRing.OfCommSemiring.instCommutativeHMul (α : Type u) [CommSemiring α] : Std.Commutative fun (x1 x2 : α) => x1 * x2

theorem Lean.Grind.CommRing.OfCommSemiring.mul_comm {α : Type u} [CommSemiring α] (a b : Ring.OfSemiring.Q α) : Ring.OfSemiring.mul a b = Ring.OfSemiring.mul b a

@[instance_reducible, instance 10000]

instance Lean.Grind.CommRing.OfCommSemiring.ofCommSemiring {α : Type u} [CommSemiring α] : CommRing (Ring.OfSemiring.Q α)

Equations

• Lean.Grind.CommRing.OfCommSemiring.ofCommSemiring = { toRing := Lean.Grind.Ring.OfSemiring.ofSemiring, mul_comm := ⋯ }

@[instance_reducible, instance 10000]

instance Lean.Grind.CommRing.OfCommSemiring.instAddQ {α : Type u} [CommSemiring α] [CommRing (Ring.OfSemiring.Q α)] : Add (Ring.OfSemiring.Q α)

Equations

• Lean.Grind.CommRing.OfCommSemiring.instAddQ = inferInstance

@[instance_reducible, instance 10000]

instance Lean.Grind.CommRing.OfCommSemiring.instSubQ {α : Type u} [CommSemiring α] [CommRing (Ring.OfSemiring.Q α)] : Sub (Ring.OfSemiring.Q α)

Equations

• Lean.Grind.CommRing.OfCommSemiring.instSubQ = inferInstance

@[instance_reducible, instance 10000]

instance Lean.Grind.CommRing.OfCommSemiring.instMulQ {α : Type u} [CommSemiring α] [CommRing (Ring.OfSemiring.Q α)] : Mul (Ring.OfSemiring.Q α)

Equations

• Lean.Grind.CommRing.OfCommSemiring.instMulQ = inferInstance

@[instance_reducible, instance 10000]

instance Lean.Grind.CommRing.OfCommSemiring.instNegQ {α : Type u} [CommSemiring α] [CommRing (Ring.OfSemiring.Q α)] : Neg (Ring.OfSemiring.Q α)

Equations

• Lean.Grind.CommRing.OfCommSemiring.instNegQ = inferInstance

@[instance_reducible, instance 10000]

instance Lean.Grind.CommRing.OfCommSemiring.instOfNatQ {α : Type u} [CommSemiring α] {n : Nat} [CommRing (Ring.OfSemiring.Q α)] : OfNat (Ring.OfSemiring.Q α) n

Equations

• Lean.Grind.CommRing.OfCommSemiring.instOfNatQ = inferInstance

@[instance_reducible, instance 10000]

instance Lean.Grind.CommRing.OfCommSemiring.instNatCastQ {α : Type u} [CommSemiring α] [CommRing (Ring.OfSemiring.Q α)] : NatCast (Ring.OfSemiring.Q α)

Equations

• Lean.Grind.CommRing.OfCommSemiring.instNatCastQ = inferInstance

@[instance_reducible, instance 10000]

instance Lean.Grind.CommRing.OfCommSemiring.instIntCastQ {α : Type u} [CommSemiring α] [CommRing (Ring.OfSemiring.Q α)] : IntCast (Ring.OfSemiring.Q α)

Equations

• Lean.Grind.CommRing.OfCommSemiring.instIntCastQ = inferInstance

@[instance_reducible, instance 10000]

instance Lean.Grind.CommRing.OfCommSemiring.instHPowQNat {α : Type u} [CommSemiring α] [CommRing (Ring.OfSemiring.Q α)] : HPow (Ring.OfSemiring.Q α) Nat (Ring.OfSemiring.Q α)

Equations

• Lean.Grind.CommRing.OfCommSemiring.instHPowQNat = inferInstance

def Lean.Grind.CommRing.OfCommSemiring.toQUnexpander : PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.