mathlib3

2412b97f - feat(algebra/quaternion_basis): add a quaternion version of complex.lift (#8551)

feat(algebra/quaternion_basis): add a quaternion version of complex.lift (#8551) This is some prework to show `clifford_algebra (Q c₁ c₂) ≃ₐ[R] ℍ[R,c₁,c₂]` for an appropriate `Q`. For `complex.lift : {I' // I' * I' = -1} ≃ (ℂ →ₐ[ℝ] A)`, we could just use a subtype. For quaternions, we now have two generators and three relations, so a subtype isn't particularly viable any more; so instead this commit creates a new `quaternion_algebra.basis` structure.