Theorem: TensorProduct.smul_rTensor (DividedPowers/PolynomialMap/Homogeneous.lean)

State before:
R✝ : Type u_1
inst✝⁹ : CommSemiring R✝
M✝ : Type u_2
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
R : Type u_3
inst✝⁶ : CommSemiring R
M : Type u_4
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : Semiring S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
m : S ⊗[R] M
⊢ φ s • (rTensor M φ.toLinearMap) m = (rTensor M φ.toLinearMap) (s • m)
Tactic:
induction m using TensorProduct.induction_on with
| zero => simp
| tmul s' m =>
  simp only [rTensor_tmul, AlgHom.toLinearMap_apply, smul_tmul', smul_eq_mul, _root_.map_mul]
| add m m' hm hm' => simp [hm, hm']
State after:
no goals

State before:
case zero
R✝ : Type u_1
inst✝⁹ : CommSemiring R✝
M✝ : Type u_2
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
R : Type u_3
inst✝⁶ : CommSemiring R
M : Type u_4
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : Semiring S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
⊢ φ s • (rTensor M φ.toLinearMap) 0 = (rTensor M φ.toLinearMap) (s • 0)
Tactic:
simp
State after:
no goals

State before:
case tmul
R✝ : Type u_1
inst✝⁹ : CommSemiring R✝
M✝ : Type u_2
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
R : Type u_3
inst✝⁶ : CommSemiring R
M : Type u_4
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : Semiring S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s s' : S
m : M
⊢ φ s • (rTensor M φ.toLinearMap) (s' ⊗ₜ[R] m) = (rTensor M φ.toLinearMap) (s • s' ⊗ₜ[R] m)
Tactic:
simp only [rTensor_tmul, AlgHom.toLinearMap_apply, smul_tmul', smul_eq_mul, _root_.map_mul]
State after:
no goals

State before:
case add
R✝ : Type u_1
inst✝⁹ : CommSemiring R✝
M✝ : Type u_2
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
R : Type u_3
inst✝⁶ : CommSemiring R
M : Type u_4
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_5
inst✝³ : Semiring S
inst✝² : Algebra R S
T : Type u_6
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
m m' : S ⊗[R] M
hm : φ s • (rTensor M φ.toLinearMap) m = (rTensor M φ.toLinearMap) (s • m)
hm' : φ s • (rTensor M φ.toLinearMap) m' = (rTensor M φ.toLinearMap) (s • m')
⊢ φ s • (rTensor M φ.toLinearMap) (m + m') = (rTensor M φ.toLinearMap) (s • (m + m'))
Tactic:
simp [hm, hm']
State after:
no goals