Theorems · Theorem · ring theory

QuaternionAlgebra.hom_ext

∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  ⦃f g : QuaternionAlgebra R c₁ c₂ c₃ →ₐ[R] A⦄,
  f (QuaternionAlgebra.Basis.self R).i = g (QuaternionAlgebra.Basis.self R).i →
    f (QuaternionAlgebra.Basis.self R).j = g (QuaternionAlgebra.Basis.self R).j → f = g

Two R-algebra morphisms from a quaternion algebra are equal if they agree on i and j.

Defined in

Mathlib.Algebra.QuaternionBasis

Cited by

3 results in Mathlib

Foundations

Depth 49 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingRingAlgebra