no goals
R : Type u_1
inst✝¹⁶ : CommSemiring R
R' : Type u_4
inst✝¹⁵ : Monoid R'
R'' : Type ?u.221106
inst✝¹⁴ : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.221118
Q : Type ?u.221121
S : Type ?u.221124
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
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
x : M ⊗[R] N
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
⊢ 1 • 0 = 0
rw [TensorProduct.smul_zero]
no goals
R : Type u_1
inst✝¹⁶ : CommSemiring R
R' : Type u_4
inst✝¹⁵ : Monoid R'
R'' : Type ?u.221106
inst✝¹⁴ : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.221118
Q : Type ?u.221121
S : Type ?u.221124
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
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
x : M ⊗[R] N
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
m : M
n : N
⊢ 1 • m ⊗ₜ[R] n = m ⊗ₜ[R] n
rw [this, one_smul]
no goals
R : Type u_1
inst✝¹⁶ : CommSemiring R
R' : Type u_4
inst✝¹⁵ : Monoid R'
R'' : Type ?u.221106
inst✝¹⁴ : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.221118
Q : Type ?u.221121
S : Type ?u.221124
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
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
x✝ : M ⊗[R] N
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : 1 • x = x
ihy : 1 • y = y
⊢ 1 • (x + y) = x + y
rw [TensorProduct.smul_add, ihx, ihy]