Quadratic algebras: involution, norm, trace, and change of generator.

Let R be a commutative ring. We define:

• QuadraticAlgebra.star: the quadratic involution

• QuadraticAlgebra.norm: the norm

• QuadraticAlgebra.trace: the trace, as an R-linear map

• QuadraticAlgebra.changeGenerator and QuadraticAlgebra.changeGeneratorEquiv: the R-algebra map, respectively isomorphism (when u is a unit), induced by the change of generator ω ↦ u • ω + k

We prove:

• QuadraticAlgebra.isUnit_iff_norm_isUnit: w : QuadraticAlgebra R a b is a unit iff w.norm is a unit in R.

• QuadraticAlgebra.norm_mem_nonZeroDivisors_iff: w : QuadraticAlgebra R a b isn't a zero divisor iff w.norm isn't a zero divisor in R.

• If K is a field, and ∀ r, r ^ 2 ≠ a + b * r, then QuadraticAlgebra K a b is a field.

def QuadraticAlgebra.omega {R : Type u_2} {a b : R} [Zero R] [One R] : QuadraticAlgebra R a b

The representative of the root in the quadratic algebra

def QuadraticAlgebra.termω : Lean.ParserDescr

the canonical element ⟨0, 1⟩ in a quadratic algebra QuadraticAlgebra R a b.

@[simp]

theorem QuadraticAlgebra.re_omega {R : Type u_2} {a b : R} [Zero R] [One R] : omega.re = 0

@[simp]

theorem QuadraticAlgebra.im_omega {R : Type u_2} {a b : R} [Zero R] [One R] : omega.im = 1

@[deprecated QuadraticAlgebra.re_omega (since := "2026-08-13")]

theorem QuadraticAlgebra.omega_re {R : Type u_2} {a b : R} [Zero R] [One R] : omega.re = 0

Alias of QuadraticAlgebra.re_omega.

@[deprecated QuadraticAlgebra.im_omega (since := "2026-08-13")]

theorem QuadraticAlgebra.omega_im {R : Type u_2} {a b : R} [Zero R] [One R] : omega.im = 1

Alias of QuadraticAlgebra.im_omega.

theorem QuadraticAlgebra.omega_mul_omega_eq_mk {R : Type u_2} {a b : R} [CommSemiring R] : omega * omega = { re := a, im := b }

theorem QuadraticAlgebra.omega_mul_omega_eq_add {R : Type u_2} {a b : R} [CommSemiring R] : omega * omega = a • 1 + b • omega

theorem QuadraticAlgebra.omega_pow_two_eq_add {R : Type u_2} {a b : R} [CommSemiring R] : omega ^ 2 = a • 1 + b • omega

theorem QuadraticAlgebra.omega_mul_omega_eq_algebraMap {R : Type u_2} {a b : R} [CommSemiring R] : omega * omega = (algebraMap R (QuadraticAlgebra R a b)) a + (algebraMap R (QuadraticAlgebra R a b)) b * omega

@[simp]

theorem QuadraticAlgebra.basis_apply_one {R : Type u_2} {a b : R} [CommSemiring R] : (basis a b) 1 = omega

@[simp]

theorem QuadraticAlgebra.omega_mul_mk {R : Type u_2} {a b : R} [CommSemiring R] (x y : R) : omega * { re := x, im := y } = { re := a * y, im := x + b * y }

@[simp]

theorem QuadraticAlgebra.omega_mul_algebraMap_mul_mk {R : Type u_2} {a b : R} [CommSemiring R] (n x y : R) : omega * (algebraMap R (QuadraticAlgebra R a b)) n * { re := x, im := y } = { re := a * n * y, im := n * x + n * b * y }

theorem QuadraticAlgebra.mk_eq_add_smul_omega {R : Type u_2} {a b : R} [CommSemiring R] (x y : R) : { re := x, im := y } = (algebraMap R (QuadraticAlgebra R a b)) x + y • omega

theorem QuadraticAlgebra.re_smul_add_im_smul {R : Type u_2} {a b : R} [CommSemiring R] (x : QuadraticAlgebra R a b) : x.re • 1 + x.im • omega = x

Decomposition of an element of a quadratic algebra in the basis (1, ω).

theorem QuadraticAlgebra.algHom_ext {R : Type u_2} {a b : R} [CommSemiring R] {A : Type u_3} [Ring A] [Algebra R A] {f g : QuadraticAlgebra R a b →ₐ[R] A} (h : f omega = g omega) : f = g

theorem QuadraticAlgebra.algHom_ext_iff {R : Type u_2} {a b : R} [CommSemiring R] {A : Type u_3} [Ring A] [Algebra R A] {f g : QuadraticAlgebra R a b →ₐ[R] A} : f = g ↔ f omega = g omega

def QuadraticAlgebra.lift {R : Type u_2} {a b : R} [CommSemiring R] {A : Type u_3} [Ring A] [Algebra R A] : { u : A // u * u = a • 1 + b • u } ≃ (QuadraticAlgebra R a b →ₐ[R] A)

The unique AlgHom from QuadraticAlgebra R a b to an R-algebra A, constructed by replacing ω with the provided root. Conversely, this associates to every algebra morphism QuadraticAlgebra R a b →ₐ[R] A a value of ω in A.

@[simp]

theorem QuadraticAlgebra.lift_symm_apply_coe {R : Type u_2} {a b : R} [CommSemiring R] {A : Type u_3} [Ring A] [Algebra R A] (f : QuadraticAlgebra R a b →ₐ[R] A) : ↑(lift.symm f) = f omega

@[simp]

theorem QuadraticAlgebra.lift_apply_apply {R : Type u_2} {a b : R} [CommSemiring R] {A : Type u_3} [Ring A] [Algebra R A] (u : { u : A // u * u = a • 1 + b • u }) (z : QuadraticAlgebra R a b) : (lift u) z = z.re • 1 + z.im • ↑u

theorem QuadraticAlgebra.adjoin_omega_eq_top {R : Type u_2} {a b : R} [CommSemiring R] : R[omega] = ⊤

A quadratic algebra is generated by ω.

theorem QuadraticAlgebra.range_lift {R : Type u_2} {a b : R} [CommSemiring R] {A : Type u_3} [Ring A] [Algebra R A] {u : A} (h : u * u = a • 1 + b • u) : (lift ⟨u, h⟩).range = R[u]

The range of lift ⟨u, h⟩ is the subalgebra of A generated by u.

theorem QuadraticAlgebra.lift_surjective_iff {R : Type u_2} {a b : R} [CommSemiring R] {A : Type u_3} [Ring A] [Algebra R A] {u : A} (h : u * u = a • 1 + b • u) : Function.Surjective ⇑(lift ⟨u, h⟩) ↔ R[u] = ⊤

lift ⟨u, h⟩ is surjective iff u generates A as an R-algebra.

theorem QuadraticAlgebra.lift_injective_iff {R : Type u_2} {a b : R} [CommRing R] {A : Type u_3} [Ring A] [Algebra R A] {u : A} (h : u * u = a • 1 + b • u) : Function.Injective ⇑(lift ⟨u, h⟩) ↔ LinearIndependent R ![1, u]

lift ⟨u, h⟩ is injective iff 1 and u are R-linearly independent.

@[instance_reducible]

instance QuadraticAlgebra.instStar {R : Type u_2} {a b : R} [CommRing R] : Star (QuadraticAlgebra R a b)

Conjugation in QuadraticAlgebra R a b. The conjugate of x + y ω is x + y ω' = (x + b * y) - y ω.

@[simp]

theorem QuadraticAlgebra.star_mk {R : Type u_2} {a b : R} [CommRing R] (x y : R) : star { re := x, im := y } = { re := x + b * y, im := -y }

@[simp]

theorem QuadraticAlgebra.re_star {R : Type u_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : (star z).re = z.re + b * z.im

@[simp]

theorem QuadraticAlgebra.im_star {R : Type u_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : (star z).im = -z.im

theorem QuadraticAlgebra.mul_star {R : Type u_2} {a b : R} [CommRing R] (x y : R) : { re := x, im := y } * star { re := x, im := y } = (algebraMap R (QuadraticAlgebra R a b)) x * (algebraMap R (QuadraticAlgebra R a b)) x + (algebraMap R (QuadraticAlgebra R a b)) b * (algebraMap R (QuadraticAlgebra R a b)) x * (algebraMap R (QuadraticAlgebra R a b)) y - (algebraMap R (QuadraticAlgebra R a b)) a * (algebraMap R (QuadraticAlgebra R a b)) y * (algebraMap R (QuadraticAlgebra R a b)) y

@[instance_reducible]

instance QuadraticAlgebra.instStarRing {R : Type u_2} {a b : R} [CommRing R] : StarRing (QuadraticAlgebra R a b)

theorem QuadraticAlgebra.sub_star {R : Type u_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : z - star z = z.im • (omega - star omega)

z - star z is a multiple of the difference ω - star ω.

def QuadraticAlgebra.norm {R : Type u_2} {a b : R} [CommRing R] : QuadraticAlgebra R a b →* R

the norm in a quadratic algebra, as a MonoidHom.

theorem QuadraticAlgebra.norm_def {R : Type u_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : norm z = z.re * z.re + b * z.re * z.im - a * z.im * z.im

@[simp]

theorem QuadraticAlgebra.norm_zero {R : Type u_2} {a b : R} [CommRing R] : norm 0 = 0

@[simp]

theorem QuadraticAlgebra.norm_one {R : Type u_2} {a b : R} [CommRing R] : norm 1 = 1

@[simp]

theorem QuadraticAlgebra.norm_algebraMap {R : Type u_2} {a b : R} [CommRing R] (r : R) : norm ((algebraMap R (QuadraticAlgebra R a b)) r) = r ^ 2

@[simp]

theorem QuadraticAlgebra.norm_natCast {R : Type u_2} {a b : R} [CommRing R] (n : ℕ) : norm ↑n = ↑n ^ 2

@[simp]

theorem QuadraticAlgebra.norm_intCast {R : Type u_2} {a b : R} [CommRing R] (n : ℤ) : norm ↑n = ↑n ^ 2

theorem QuadraticAlgebra.algebraMap_norm_eq_mul_star {R : Type u_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : (algebraMap R (QuadraticAlgebra R a b)) (norm z) = z * star z

@[simp]

theorem QuadraticAlgebra.norm_neg {R : Type u_2} {a b : R} [CommRing R] (x : QuadraticAlgebra R a b) : norm (-x) = norm x

@[simp]

theorem QuadraticAlgebra.norm_star {R : Type u_2} {a b : R} [CommRing R] (x : QuadraticAlgebra R a b) : norm (star x) = norm x

theorem QuadraticAlgebra.isUnit_iff_norm_isUnit {R : Type u_2} {a b : R} [CommRing R] {x : QuadraticAlgebra R a b} : IsUnit x ↔ IsUnit (norm x)

theorem QuadraticAlgebra.norm_eq_one_iff_mem_unitary {R : Type u_2} {a b : R} [CommRing R] {z : QuadraticAlgebra R a b} : norm z = 1 ↔ z ∈ unitary (QuadraticAlgebra R a b)

An element of QuadraticAlgebra R a b has norm equal to 1 if and only if it is contained in the submonoid of unitary elements.

theorem QuadraticAlgebra.norm_eq_one {R : Type u_2} {a b : R} [CommRing R] {z : QuadraticAlgebra R a b} : z ∈ unitary (QuadraticAlgebra R a b) → norm z = 1

Alias of the reverse direction of QuadraticAlgebra.norm_eq_one_iff_mem_unitary.

---

An element of QuadraticAlgebra R a b has norm equal to 1 if and only if it is contained in the submonoid of unitary elements.

theorem QuadraticAlgebra.mem_unitary {R : Type u_2} {a b : R} [CommRing R] {z : QuadraticAlgebra R a b} : norm z = 1 → z ∈ unitary (QuadraticAlgebra R a b)

Alias of the forward direction of QuadraticAlgebra.norm_eq_one_iff_mem_unitary.

---

An element of QuadraticAlgebra R a b has norm equal to 1 if and only if it is contained in the submonoid of unitary elements.

theorem QuadraticAlgebra.mker_norm_eq_unitary {R : Type u_2} {a b : R} [CommRing R] : MonoidHom.mker norm = unitary (QuadraticAlgebra R a b)

The kernel of the norm map on QuadraticAlgebra R a b equals the submonoid of unitary elements.

theorem QuadraticAlgebra.algebraMap_mem_nonZeroDivisors_iff {R : Type u_2} {a b : R} [CommRing R] {r : R} : (algebraMap R (QuadraticAlgebra R a b)) r ∈ nonZeroDivisors (QuadraticAlgebra R a b) ↔ r ∈ nonZeroDivisors R

theorem QuadraticAlgebra.star_mem_nonZeroDivisors {R : Type u_2} {a b : R} [CommRing R] {z : QuadraticAlgebra R a b} (hz : z ∈ nonZeroDivisors (QuadraticAlgebra R a b)) : star z ∈ nonZeroDivisors (QuadraticAlgebra R a b)

theorem QuadraticAlgebra.star_mem_nonZeroDivisors_iff {R : Type u_2} {a b : R} [CommRing R] {z : QuadraticAlgebra R a b} : star z ∈ nonZeroDivisors (QuadraticAlgebra R a b) ↔ z ∈ nonZeroDivisors (QuadraticAlgebra R a b)

theorem QuadraticAlgebra.norm_mem_nonZeroDivisors_iff {R : Type u_2} {a b : R} [CommRing R] {z : QuadraticAlgebra R a b} : norm z ∈ nonZeroDivisors R ↔ z ∈ nonZeroDivisors (QuadraticAlgebra R a b)

def QuadraticAlgebra.trace {R : Type u_2} {a b : R} [CommRing R] : QuadraticAlgebra R a b →ₗ[R] R

The trace in a quadratic algebra, as an R-linear map.

theorem QuadraticAlgebra.trace_def {R : Type u_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : trace z = 2 * z.re + b * z.im

@[simp]

theorem QuadraticAlgebra.trace_algebraMap {R : Type u_2} {a b : R} [CommRing R] (r : R) : trace ((algebraMap R (QuadraticAlgebra R a b)) r) = 2 * r

@[simp]

theorem QuadraticAlgebra.trace_natCast {R : Type u_2} {a b : R} [CommRing R] (n : ℕ) : trace ↑n = 2 * ↑n

@[simp]

theorem QuadraticAlgebra.trace_intCast {R : Type u_2} {a b : R} [CommRing R] (n : ℤ) : trace ↑n = 2 * ↑n

@[simp]

theorem QuadraticAlgebra.trace_omega {R : Type u_2} {a b : R} [CommRing R] : trace omega = b

@[simp]

theorem QuadraticAlgebra.trace_one {R : Type u_2} {a b : R} [CommRing R] : trace 1 = 2

@[simp]

theorem QuadraticAlgebra.trace_star {R : Type u_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : trace (star z) = trace z

theorem QuadraticAlgebra.algebraMap_trace_eq_add_star {R : Type u_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : (algebraMap R (QuadraticAlgebra R a b)) (trace z) = z + star z

z + star z is the trace of z.

theorem QuadraticAlgebra.star_eq {R : Type u_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : star z = (algebraMap R (QuadraticAlgebra R a b)) (trace z) - z

The conjugate of z is trace z - z.

theorem QuadraticAlgebra.sq_sub_trace_smul_add_norm_eq_zero {R : Type u_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : z ^ 2 - trace z • z + (algebraMap R (QuadraticAlgebra R a b)) (norm z) = 0

Every element of a quadratic algebra satisfies its characteristic equation.

theorem QuadraticAlgebra.sq_eq_trace_smul_sub_norm {R : Type u_2} {a b : R} [CommRing R] (z : QuadraticAlgebra R a b) : z ^ 2 = trace z • z - (algebraMap R (QuadraticAlgebra R a b)) (norm z)

def QuadraticAlgebra.changeGenerator {R : Type u_2} [CommRing R] (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2) (hb : b' = u * b + 2 * k) : QuadraticAlgebra R a' b' →ₐ[R] QuadraticAlgebra R a b

The R-algebra map induced by the change of generator ω ↦ u • ω + k, see changeGenerator_omega.

@[simp]

theorem QuadraticAlgebra.re_changeGenerator_apply {R : Type u_2} [CommRing R] (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2) (hb : b' = u * b + 2 * k) (z : QuadraticAlgebra R a' b') : ((changeGenerator a b u k ha hb) z).re = z.re + z.im * k

@[simp]

theorem QuadraticAlgebra.im_changeGenerator_apply {R : Type u_2} [CommRing R] (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2) (hb : b' = u * b + 2 * k) (z : QuadraticAlgebra R a' b') : ((changeGenerator a b u k ha hb) z).im = z.im * u

@[simp]

theorem QuadraticAlgebra.changeGenerator_omega {R : Type u_2} [CommRing R] (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2) (hb : b' = u * b + 2 * k) : (changeGenerator a b u k ha hb) omega = u • omega + (algebraMap R (QuadraticAlgebra R a b)) k

theorem QuadraticAlgebra.changeGenerator_injective {R : Type u_2} [CommRing R] (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2) (hb : b' = u * b + 2 * k) (hu : IsRegular u) : Function.Injective ⇑(changeGenerator a b u k ha hb)

def QuadraticAlgebra.changeGeneratorEquiv {R : Type u_2} [CommRing R] (a b : R) (u : Rˣ) (k : R) {a' b' : R} (ha : a' = ↑u ^ 2 * a - ↑u * b * k - k ^ 2) (hb : b' = ↑u * b + 2 * k) : QuadraticAlgebra R a' b' ≃ₐ[R] QuadraticAlgebra R a b

changeGenerator along a unit u, as an isomorphism.

@[simp]

theorem QuadraticAlgebra.changeGeneratorEquiv_symm_apply {R : Type u_2} [CommRing R] (a b : R) (u : Rˣ) (k : R) {a' b' : R} (ha : a' = ↑u ^ 2 * a - ↑u * b * k - k ^ 2) (hb : b' = ↑u * b + 2 * k) (a✝ : QuadraticAlgebra R a b) : (changeGeneratorEquiv a b u k ha hb).symm a✝ = (changeGenerator a' b' (↑u⁻¹) (-(↑u⁻¹ * k)) ⋯ ⋯) a✝

@[simp]

theorem QuadraticAlgebra.changeGeneratorEquiv_apply {R : Type u_2} [CommRing R] (a b : R) (u : Rˣ) (k : R) {a' b' : R} (ha : a' = ↑u ^ 2 * a - ↑u * b * k - k ^ 2) (hb : b' = ↑u * b + 2 * k) (a✝ : QuadraticAlgebra R a' b') : (changeGeneratorEquiv a b u k ha hb) a✝ = (changeGenerator a b (↑u) k ha hb) a✝

@[deprecated QuadraticAlgebra.changeGenerator (since := "2026-08-14")]

def QuadraticAlgebra.map {R : Type u_2} [CommRing R] (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2) (hb : b' = u * b + 2 * k) : QuadraticAlgebra R a' b' →ₐ[R] QuadraticAlgebra R a b

Alias of QuadraticAlgebra.changeGenerator.

---

The R-algebra map induced by the change of generator ω ↦ u • ω + k, see changeGenerator_omega.

@[deprecated QuadraticAlgebra.changeGenerator_omega (since := "2026-08-14")]

theorem QuadraticAlgebra.map_omega {R : Type u_2} [CommRing R] (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2) (hb : b' = u * b + 2 * k) : (changeGenerator a b u k ha hb) omega = u • omega + (algebraMap R (QuadraticAlgebra R a b)) k

Alias of QuadraticAlgebra.changeGenerator_omega.

@[deprecated QuadraticAlgebra.changeGenerator_injective (since := "2026-08-14")]

theorem QuadraticAlgebra.map_injective {R : Type u_2} [CommRing R] (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2) (hb : b' = u * b + 2 * k) (hu : IsRegular u) : Function.Injective ⇑(changeGenerator a b u k ha hb)

Alias of QuadraticAlgebra.changeGenerator_injective.

@[deprecated QuadraticAlgebra.changeGeneratorEquiv (since := "2026-08-14")]

def QuadraticAlgebra.mapEquiv {R : Type u_2} [CommRing R] (a b : R) (u : Rˣ) (k : R) {a' b' : R} (ha : a' = ↑u ^ 2 * a - ↑u * b * k - k ^ 2) (hb : b' = ↑u * b + 2 * k) : QuadraticAlgebra R a' b' ≃ₐ[R] QuadraticAlgebra R a b

Alias of QuadraticAlgebra.changeGeneratorEquiv.

---

changeGenerator along a unit u, as an isomorphism.

theorem QuadraticAlgebra.norm_eq_zero_iff_eq_zero {K : Type u_1} [Field K] {a b : K} [Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)] {z : QuadraticAlgebra K a b} : norm z = 0 ↔ z = 0

@[instance_reducible]

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

@[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_reducible]

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

@[simp]

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

@[simp]

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

@[instance_reducible]

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

theorem QuadraticAlgebra.inv_def {K : Type u_1} [Field K] {a b : K} (z : QuadraticAlgebra K a b) : z⁻¹ = (norm z)⁻¹ • star z

@[simp]

theorem QuadraticAlgebra.re_inv {K : Type u_1} [Field K] {a b : K} (z : QuadraticAlgebra K a b) : z⁻¹.re = (norm z)⁻¹ * (z.re + b * z.im)

@[simp]

theorem QuadraticAlgebra.im_inv {K : Type u_1} [Field K] {a b : K} (z : QuadraticAlgebra K a b) : z⁻¹.im = -((norm z)⁻¹ * z.im)

@[instance_reducible]

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

theorem QuadraticAlgebra.div_def {K : Type u_1} [Field K] {a b : K} (w z : QuadraticAlgebra K a b) : w / z = w * z⁻¹

@[simp]

theorem QuadraticAlgebra.im_div {K : Type u_1} [Field K] {a b : K} (w z : QuadraticAlgebra K a b) : (w / z).im = -(w.re * ((norm z)⁻¹ * z.im)) + w.im * ((norm z)⁻¹ * (z.re + b * z.im)) + -(b * w.im * ((norm z)⁻¹ * z.im))

@[simp]

theorem QuadraticAlgebra.re_div {K : Type u_1} [Field K] {a b : K} (w z : QuadraticAlgebra K a b) : (w / z).re = w.re * ((norm z)⁻¹ * (z.re + b * z.im)) + -(a * w.im * ((norm z)⁻¹ * z.im))

@[instance_reducible]

instance QuadraticAlgebra.instField {K : Type u_1} [Field K] {a b : K} [Hab : 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.

instance QuadraticAlgebra.instFactForallNeHPowOfNatHAddHMul {K : Type u_1} [Field K] {a : K} [Fact ¬IsSquare a] : Fact (∀ (r : K), r ^ 2 ≠ a + 0 * r)

When b = 0, the Field instance is inferable from ¬ IsSquare a alone: it provides the no-root condition ∀ r, r ^ 2 ≠ a + 0 * r.