case h
R : Type u
A₁ : Type v
A₂ : Type w
A₃ : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A₁
inst✝⁴ : Semiring A₂
inst✝³ : Semiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
l : A₁ ≃ₗ[R] A₂
map_mul✝ : ∀ (x y : A₁), ↑l (x * y) = ↑l x * ↑l y
commutes✝ : ∀ (r : R), ↑l (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r
map_mul : ∀ (x y : A₁), ↑(toLinearEquiv e) (x * y) = ↑(toLinearEquiv e) x * ↑(toLinearEquiv e) y
commutes : ∀ (r : R), ↑(toLinearEquiv e) (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r
a✝ : A₁
⊢ ↑(ofLinearEquiv (toLinearEquiv e) map_mul commutes) a✝ = ↑e a✝
R : Type u
A₁ : Type v
A₂ : Type w
A₃ : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A₁
inst✝⁴ : Semiring A₂
inst✝³ : Semiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
l : A₁ ≃ₗ[R] A₂
map_mul✝ : ∀ (x y : A₁), ↑l (x * y) = ↑l x * ↑l y
commutes✝ : ∀ (r : R), ↑l (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r
map_mul : ∀ (x y : A₁), ↑(toLinearEquiv e) (x * y) = ↑(toLinearEquiv e) x * ↑(toLinearEquiv e) y
commutes : ∀ (r : R), ↑(toLinearEquiv e) (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r
⊢ ofLinearEquiv (toLinearEquiv e) map_mul commutes = e
ext
no goals
case h
R : Type u
A₁ : Type v
A₂ : Type w
A₃ : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A₁
inst✝⁴ : Semiring A₂
inst✝³ : Semiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
l : A₁ ≃ₗ[R] A₂
map_mul✝ : ∀ (x y : A₁), ↑l (x * y) = ↑l x * ↑l y
commutes✝ : ∀ (r : R), ↑l (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r
map_mul : ∀ (x y : A₁), ↑(toLinearEquiv e) (x * y) = ↑(toLinearEquiv e) x * ↑(toLinearEquiv e) y
commutes : ∀ (r : R), ↑(toLinearEquiv e) (↑(algebraMap R A₁) r) = ↑(algebraMap R A₂) r
a✝ : A₁
⊢ ↑(ofLinearEquiv (toLinearEquiv e) map_mul commutes) a✝ = ↑e a✝
rfl