Theorems · Inductive type · ring theory

QuaternionAlgebra.Basis

{R : Type u_1} → (A : Type u_2) → [inst : CommRing R] → [inst_1 : Ring A] → [Algebra R A] → R → R → R → Type u_2

A quaternion basis contains the information both sufficient and necessary to construct an R-algebra homomorphism from ℍ[R,c₁,c₂,c₃] to A; or equivalently, a surjective R-algebra homomorphism from ℍ[R,c₁,c₂,c₃] to an R-subalgebra of A. Note that for definitional convenience, k is provided as a field even though i_mul_j fully determines it.

Defined in

Mathlib.Algebra.QuaternionBasis

Cited by

28 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CommRingRingAlgebra