Theorems · Theorem · ring theory
QuaternionAlgebra.ext
∀ {R : Type u_1} {a b c : R} {x y : QuaternionAlgebra R a b c},
x.re = y.re → x.imI = y.imI → x.imJ = y.imJ → x.imK = y.imK → x = y- Defined in
- Mathlib.Algebra.Quaternion
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- QuaternionAlgebrastatement and proof · cited by 174
- QuaternionAlgebra.restatement and proof · cited by 117
- QuaternionAlgebra.imIstatement and proof · cited by 91
- QuaternionAlgebra.imJstatement and proof · cited by 80
- QuaternionAlgebra.imKstatement and proof · cited by 78
Cited by21
Results whose statement or proof uses this declaration.
- QuaternionAlgebra.coe_mulproof · cited by 8
- Quaternion.extproof · cited by 6
- QuaternionAlgebra.coe_addproof · cited by 4
- QuaternionAlgebra.self_add_star'proof · cited by 3
- QuaternionAlgebra.coe_negproof · cited by 2
- QuaternionAlgebra.star_coeproof · cited by 2
- QuaternionAlgebra.star_mul_eq_coeproof · cited by 2
- QuaternionAlgebra.coe_smulproof · cited by 1
- QuaternionAlgebra.re_add_improof · cited by 1
- QuaternionAlgebra.im_addproof · cited by 1
- QuaternionAlgebra.im_negproof · cited by 1
- QuaternionAlgebra.im_smulproof · cited by 1