case H
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
φ : A →ₐ[R] B
map_one : ↑(toLinearMap φ) 1 = 1
map_mul : ∀ (x y : A), ↑(toLinearMap φ) (x * y) = ↑(toLinearMap φ) x * ↑(toLinearMap φ) y
x✝ : A
⊢ ↑(ofLinearMap (toLinearMap φ) map_one map_mul) x✝ = ↑φ x✝
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
φ : A →ₐ[R] B
map_one : ↑(toLinearMap φ) 1 = 1
map_mul : ∀ (x y : A), ↑(toLinearMap φ) (x * y) = ↑(toLinearMap φ) x * ↑(toLinearMap φ) y
⊢ ofLinearMap (toLinearMap φ) map_one map_mul = φ
ext
no goals
case H
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
φ : A →ₐ[R] B
map_one : ↑(toLinearMap φ) 1 = 1
map_mul : ∀ (x y : A), ↑(toLinearMap φ) (x * y) = ↑(toLinearMap φ) x * ↑(toLinearMap φ) y
x✝ : A
⊢ ↑(ofLinearMap (toLinearMap φ) map_one map_mul) x✝ = ↑φ x✝
rfl