no goals
k : Type u_1
inst✝⁴ : CommRing k
R : Type u_2
inst✝³ : Ring R
inst✝² : Algebra k R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module k M
ι : Type u_4
b : Basis ι k M
r : R
x : R ⊗[k] M
⊢ ↑(basisAux R b) (r • 0) = r • ↑(basisAux R b) 0
simp
no goals
k : Type u_1
inst✝⁴ : CommRing k
R : Type u_2
inst✝³ : Ring R
inst✝² : Algebra k R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module k M
ι : Type u_4
b : Basis ι k M
r : R
x✝ : R ⊗[k] M
x : R
y : M
⊢ ↑(basisAux R b) (r • x ⊗ₜ[k] y) = r • ↑(basisAux R b) (x ⊗ₜ[k] y)
simp only [TensorProduct.smul_tmul', basisAux_tmul, smul_assoc]
no goals
k : Type u_1
inst✝⁴ : CommRing k
R : Type u_2
inst✝³ : Ring R
inst✝² : Algebra k R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module k M
ι : Type u_4
b : Basis ι k M
r : R
x✝ x y : R ⊗[k] M
hx : ↑(basisAux R b) (r • x) = r • ↑(basisAux R b) x
hy : ↑(basisAux R b) (r • y) = r • ↑(basisAux R b) y
⊢ ↑(basisAux R b) (r • (x + y)) = r • ↑(basisAux R b) (x + y)
simp [hx, hy]