instance QuadraticAlgebra.instNNRatCast_formalConjecturesForMathlib {K : Type u_1} [Field K] {a b : K} : NNRatCast (QuadraticAlgebra K a b)

Equations

• QuadraticAlgebra.instNNRatCast_formalConjecturesForMathlib = { nnratCast := fun (q : ℚ≥0) => { re := ↑q, im := 0 } }

@[simp]

theorem QuadraticAlgebra.re_nnratCast {K : Type u_1} [Field K] {a b : K} (q : ℚ≥0) : (NNRatCast.nnratCast q).re = ↑q

@[simp]

theorem QuadraticAlgebra.im_nnratCast {K : Type u_1} [Field K] {a b : K} (q : ℚ≥0) : (NNRatCast.nnratCast q).im = 0

instance QuadraticAlgebra.instRatCast_formalConjecturesForMathlib {K : Type u_1} [Field K] {a b : K} : RatCast (QuadraticAlgebra K a b)

Equations

• QuadraticAlgebra.instRatCast_formalConjecturesForMathlib = { ratCast := fun (q : ℚ) => { re := ↑q, im := 0 } }

@[simp]

theorem QuadraticAlgebra.im_ratCast {K : Type u_1} [Field K] {a b : K} (q : ℚ) : (RatCast.ratCast q).im = 0

@[simp]

theorem QuadraticAlgebra.re_ratCast {K : Type u_1} [Field K] {a b : K} (q : ℚ) : (RatCast.ratCast q).re = ↑q

instance QuadraticAlgebra.instField' {K : Type u_1} [Field K] {a b : K} [Fact (∀ (r : K), r ^ 2 ≠ a + b * r)] : Field (QuadraticAlgebra K a b)

If K is a field and there is no r : K such that r ^ 2 = a + b * r, then QuadraticAlgebra K a b is a field.

Equations

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