no goals
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.601904
inst✝¹³ : Monoid R'
R'' : Type ?u.601910
inst✝¹² : Semiring R''
M : Type u_3
N : Type u_2
P : Type u_4
Q : Type ?u.601925
S : Type ?u.601928
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] N →ₗ[R] P
g h : M ⊗[R] N →ₗ[R] P
H : ∀ (x : M) (y : N), ↑g (x ⊗ₜ[R] y) = ↑h (x ⊗ₜ[R] y)
z : M ⊗[R] N
⊢ ↑g 0 = ↑h 0
simp_rw [LinearMap.map_zero]
no goals
R : Type u_1
inst✝¹⁴ : CommSemiring R
R' : Type ?u.601904
inst✝¹³ : Monoid R'
R'' : Type ?u.601910
inst✝¹² : Semiring R''
M : Type u_3
N : Type u_2
P : Type u_4
Q : Type ?u.601925
S : Type ?u.601928
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : AddCommMonoid S
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Module R S
inst✝¹ : DistribMulAction R' M
inst✝ : Module R'' M
f : M →ₗ[R] N →ₗ[R] P
g h : M ⊗[R] N →ₗ[R] P
H : ∀ (x : M) (y : N), ↑g (x ⊗ₜ[R] y) = ↑h (x ⊗ₜ[R] y)
z x y : M ⊗[R] N
ihx : ↑g x = ↑h x
ihy : ↑g y = ↑h y
⊢ ↑g (x + y) = ↑h (x + y)
rw [g.map_add, h.map_add, ihx, ihy]