ι : Type u_2
ι' : Type ?u.297290
R : Type u_4
R₂ : Type ?u.297296
K : Type ?u.297299
M : Type u_1
M' : Type ?u.297305
M'' : Type ?u.297308
V : Type u
V' : Type ?u.297313
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
b b₁ : Basis ι R M
i✝ : ι
c : R
x : M
R' : Type u_3
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), ↑f c • x = c • x
i : ι
this : Module R' R := Module.compHom R ↑(RingEquiv.symm f)
⊢ ↑(mapCoeffs b f h).repr (↑b i) = Finsupp.single i 1
ι : Type u_2
ι' : Type ?u.297290
R : Type u_4
R₂ : Type ?u.297296
K : Type ?u.297299
M : Type u_1
M' : Type ?u.297305
M'' : Type ?u.297308
V : Type u
V' : Type ?u.297313
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
b b₁ : Basis ι R M
i✝ : ι
c : R
x : M
R' : Type u_3
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), ↑f c • x = c • x
i : ι
⊢ ↑(mapCoeffs b f h).repr (↑b i) = Finsupp.single i 1
letI : Module R' R := Module.compHom R (↑f.symm : R' →+* R)
ι : Type u_2
ι' : Type ?u.297290
R : Type u_4
R₂ : Type ?u.297296
K : Type ?u.297299
M : Type u_1
M' : Type ?u.297305
M'' : Type ?u.297308
V : Type u
V' : Type ?u.297313
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
b b₁ : Basis ι R M
i✝ : ι
c : R
x : M
R' : Type u_3
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), ↑f c • x = c • x
i : ι
this✝ : Module R' R := Module.compHom R ↑(RingEquiv.symm f)
this : IsScalarTower R' R M
⊢ ↑(mapCoeffs b f h).repr (↑b i) = Finsupp.single i 1
ι : Type u_2
ι' : Type ?u.297290
R : Type u_4
R₂ : Type ?u.297296
K : Type ?u.297299
M : Type u_1
M' : Type ?u.297305
M'' : Type ?u.297308
V : Type u
V' : Type ?u.297313
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
b b₁ : Basis ι R M
i✝ : ι
c : R
x : M
R' : Type u_3
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), ↑f c • x = c • x
i : ι
this : Module R' R := Module.compHom R ↑(RingEquiv.symm f)
⊢ ↑(mapCoeffs b f h).repr (↑b i) = Finsupp.single i 1
haveI : IsScalarTower R' R M :=
{ smul_assoc := fun x y z => by
    change (f.symm x * y) • z = x • (y • z)
    rw [mul_smul, ← h, f.apply_symm_apply] }
no goals
ι : Type u_2
ι' : Type ?u.297290
R : Type u_4
R₂ : Type ?u.297296
K : Type ?u.297299
M : Type u_1
M' : Type ?u.297305
M'' : Type ?u.297308
V : Type u
V' : Type ?u.297313
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
b b₁ : Basis ι R M
i✝ : ι
c : R
x : M
R' : Type u_3
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), ↑f c • x = c • x
i : ι
this✝ : Module R' R := Module.compHom R ↑(RingEquiv.symm f)
this : IsScalarTower R' R M
⊢ ↑(mapCoeffs b f h).repr (↑b i) = Finsupp.single i 1
simp
ι : Type u_2
ι' : Type ?u.297290
R : Type u_4
R₂ : Type ?u.297296
K : Type ?u.297299
M : Type u_1
M' : Type ?u.297305
M'' : Type ?u.297308
V : Type u
V' : Type ?u.297313
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
b b₁ : Basis ι R M
i✝ : ι
c : R
x✝ : M
R' : Type u_3
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), ↑f c • x = c • x
i : ι
this : Module R' R := Module.compHom R ↑(RingEquiv.symm f)
x : R'
y : R
z : M
⊢ (↑(RingEquiv.symm f) x * y) • z = x • y • z
ι : Type u_2
ι' : Type ?u.297290
R : Type u_4
R₂ : Type ?u.297296
K : Type ?u.297299
M : Type u_1
M' : Type ?u.297305
M'' : Type ?u.297308
V : Type u
V' : Type ?u.297313
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
b b₁ : Basis ι R M
i✝ : ι
c : R
x✝ : M
R' : Type u_3
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), ↑f c • x = c • x
i : ι
this : Module R' R := Module.compHom R ↑(RingEquiv.symm f)
x : R'
y : R
z : M
⊢ (x • y) • z = x • y • z
change (f.symm x * y) • z = x • (y • z)
no goals
ι : Type u_2
ι' : Type ?u.297290
R : Type u_4
R₂ : Type ?u.297296
K : Type ?u.297299
M : Type u_1
M' : Type ?u.297305
M'' : Type ?u.297308
V : Type u
V' : Type ?u.297313
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
b b₁ : Basis ι R M
i✝ : ι
c : R
x✝ : M
R' : Type u_3
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), ↑f c • x = c • x
i : ι
this : Module R' R := Module.compHom R ↑(RingEquiv.symm f)
x : R'
y : R
z : M
⊢ (↑(RingEquiv.symm f) x * y) • z = x • y • z
rw [mul_smul, ← h, f.apply_symm_apply]