Theorems · Inductive type · ring theory

QuadraticAlgebra

(R : Type u) → R → R → Type u

Quadratic algebra over a type with fixed coefficient where $i^2 = a + bi$, implemented as a structure with two fields, re and im. When R is a commutative ring, this is isomorphic to R[X]/(X^2-b*X-a).

Defined in

Mathlib.Algebra.QuadraticAlgebra.Defs

Cited by

123 results in Mathlib

Foundations

Depth 0 from the axioms, rests on 1 definitions · uses no axioms