R : Type u_1
A : Type u_2
B : Type ?u.73937
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ ↑(algebraMap R A) x.re + ↑(algebraMap R A) y.re + (x.imI • q.i + y.imI • q.i) + (x.imJ • q.j + y.imJ • q.j) +
      (x.imK • q.k + y.imK • q.k) =
    ↑(algebraMap R A) x.re + x.imI • q.i + x.imJ • q.j + x.imK • q.k +
      (↑(algebraMap R A) y.re + y.imI • q.i + y.imJ • q.j + y.imK • q.k)
R : Type u_1
A : Type u_2
B : Type ?u.73937
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ lift q (x + y) = lift q x + lift q y
simp [lift, add_smul]
no goals
R : Type u_1
A : Type u_2
B : Type ?u.73937
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
x y : ℍ[R,c₁,c₂]
⊢ ↑(algebraMap R A) x.re + ↑(algebraMap R A) y.re + (x.imI • q.i + y.imI • q.i) + (x.imJ • q.j + y.imJ • q.j) +
      (x.imK • q.k + y.imK • q.k) =
    ↑(algebraMap R A) x.re + x.imI • q.i + x.imJ • q.j + x.imK • q.k +
      (↑(algebraMap R A) y.re + y.imI • q.i + y.imJ • q.j + y.imK • q.k)
abel