Discriminant of a quadratic algebra

This file introduces the discriminant of a quadratic algebra QuadraticAlgebra R a b (with the convention ω² = a + b·ω), describes how it transforms under a change of generator, and derives, over a field, a criterion for QuadraticAlgebra K a b to be a field.

Main definitions

• QuadraticAlgebra.discr: the discriminant discr a b = b ^ 2 + 4 * a.

Main results

• QuadraticAlgebra.discr_changeGenerator: the discriminant scales by u ^ 2 under the change of generator ω ↦ u • ω + k.
• QuadraticAlgebra.exists_sq_eq_iff_isSquare_discr: over a ring with 2 invertible, X ^ 2 - b * X - a has a root iff discr a b is a square.
• QuadraticAlgebra.isField_iff_not_isSquare_discr: over a field with 2 ≠ 0, QuadraticAlgebra K a b is a field iff discr a b is not a square.

def QuadraticAlgebra.discr {R : Type u_1} [CommSemiring R] (a b : R) : R

The discriminant of the quadratic algebra QuadraticAlgebra R a b, that is, the discriminant b ^ 2 + 4 * a of the polynomial X ^ 2 - b * X - a.

Equations

• QuadraticAlgebra.discr a b = b ^ 2 + 4 * a

theorem QuadraticAlgebra.discr_def {R : Type u_1} [CommSemiring R] (a b : R) : discr a b = b ^ 2 + 4 * a

theorem QuadraticAlgebra.discr_changeGenerator {R : Type u_1} [CommRing R] (a b u k : R) : discr (u ^ 2 * a - u * b * k - k ^ 2) (u * b + 2 * k) = u ^ 2 * discr a b

Under the change of generator ω ↦ u • ω + k (see QuadraticAlgebra.changeGenerator), the discriminant is multiplied by u ^ 2.

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

theorem QuadraticAlgebra.discr_map {R : Type u_1} [CommRing R] (a b u k : R) : discr (u ^ 2 * a - u * b * k - k ^ 2) (u * b + 2 * k) = u ^ 2 * discr a b

Alias of QuadraticAlgebra.discr_changeGenerator.

---

Under the change of generator ω ↦ u • ω + k (see QuadraticAlgebra.changeGenerator), the discriminant is multiplied by u ^ 2.

theorem QuadraticAlgebra.algebraMap_discr {R : Type u_1} [CommRing R] (a b : R) : (algebraMap R (QuadraticAlgebra R a b)) (discr a b) = (omega - star omega) ^ 2

The discriminant is the square of the different ω - star ω.

theorem QuadraticAlgebra.exists_sq_eq_iff_isSquare_discr {R : Type u_1} [CommRing R] [Invertible 2] {a b : R} : (∃ (r : R), r ^ 2 = a + b * r) ↔ IsSquare (discr a b)

If 2 is invertible, the polynomial X ^ 2 - b * X - a has a root if and only if the discriminant is a square.

instance QuadraticAlgebra.instFactForallNeHPowOfNatHAddHMul_1 {K : Type u_2} [Field K] {a b : K} [NeZero 2] [Fact ¬IsSquare (discr a b)] : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)

theorem QuadraticAlgebra.not_isField_of_isSquare_discr {K : Type u_2} [Field K] [NeZero 2] {a b : K} (h : IsSquare (discr a b)) : ¬IsField (QuadraticAlgebra K a b)

If discr a b is a square, QuadraticAlgebra K a b is not a field.

theorem QuadraticAlgebra.isField_iff_not_isSquare_discr {K : Type u_2} [Field K] [NeZero 2] {a b : K} : IsField (QuadraticAlgebra K a b) ↔ ¬IsSquare (discr a b)

If 2 ≠ 0 in the field K, QuadraticAlgebra K a b is a field iff discr a b is not a square.