R : Type ?u.731560
inst✝² : CommRing R
M : Type ?u.731566
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
this : Module R[X] M := modulePolynomialOfEndo f
⊢ SMul R[X] M
R : Type ?u.731560
inst✝² : CommRing R
M : Type ?u.731566
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
⊢ SMul R[X] M
letI := modulePolynomialOfEndo f
no goals
R : Type ?u.731560
inst✝² : CommRing R
M : Type ?u.731566
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
this : Module R[X] M := modulePolynomialOfEndo f
⊢ SMul R[X] M
infer_instance
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
x✝ : Module R[X] M := modulePolynomialOfEndo f
⊢ IsScalarTower R R[X] M
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
⊢ IsScalarTower R R[X] M
let _ := modulePolynomialOfEndo f
case smul_assoc
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
x✝ : Module R[X] M := modulePolynomialOfEndo f
⊢ ∀ (x : R) (y : R[X]) (z : M), (x • y) • z = x • y • z
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
x✝ : Module R[X] M := modulePolynomialOfEndo f
⊢ IsScalarTower R R[X] M
constructor
case smul_assoc
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
x✝ : Module R[X] M := modulePolynomialOfEndo f
x : R
y : R[X]
z : M
⊢ (x • y) • z = x • y • z
case smul_assoc
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
x✝ : Module R[X] M := modulePolynomialOfEndo f
⊢ ∀ (x : R) (y : R[X]) (z : M), (x • y) • z = x • y • z
intro x y z
no goals
case smul_assoc
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
x✝ : Module R[X] M := modulePolynomialOfEndo f
x : R
y : R[X]
z : M
⊢ (x • y) • z = x • y • z
simp