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
f : A →ₗ[R] B
map_one : ↑f 1 = 1
map_mul : ∀ (x y : A), ↑f (x * y) = ↑f x * ↑f y
x✝ : A
⊢ ↑(toLinearMap (ofLinearMap f map_one map_mul)) x✝ = ↑f 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
f : A →ₗ[R] B
map_one : ↑f 1 = 1
map_mul : ∀ (x y : A), ↑f (x * y) = ↑f x * ↑f y
⊢ toLinearMap (ofLinearMap f map_one map_mul) = f
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
f : A →ₗ[R] B
map_one : ↑f 1 = 1
map_mul : ∀ (x y : A), ↑f (x * y) = ↑f x * ↑f y
x✝ : A
⊢ ↑(toLinearMap (ofLinearMap f map_one map_mul)) x✝ = ↑f x✝
rfl