Theorem: DividedPowerAlgebra.isHomogeneousOfDegree_gamma (DividedPowers/DPAlgebra/PolynomialMap.lean)

State before:
R : Type u
inst✝² : CommRing R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ PolynomialMap.IsHomogeneousOfDegree n (gamma R M n)
Tactic:
intro S _ _ r sm
State after:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
sm : S ⊗[R] M
⊢ (gamma R M n).toFun' S (r • sm) = r ^ n • (gamma R M n).toFun' S sm

State before:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
sm : S ⊗[R] M
⊢ (gamma R M n).toFun' S (r • sm) = r ^ n • (gamma R M n).toFun' S sm
Tactic:
simp only [gamma]
State after:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
sm : S ⊗[R] M
⊢ (dpScalarExtensionEquiv R S M).symm (dp S n (r • sm)) = r ^ n • (dpScalarExtensionEquiv R S M).symm (dp S n sm)

State before:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
sm : S ⊗[R] M
⊢ (dpScalarExtensionEquiv R S M).symm (dp S n (r • sm)) = r ^ n • (dpScalarExtensionEquiv R S M).symm (dp S n sm)
Tactic:
apply (dpScalarExtensionEquiv R S M).injective
State after:
case a
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
sm : S ⊗[R] M
⊢ (dpScalarExtensionEquiv R S M) ((dpScalarExtensionEquiv R S M).symm (dp S n (r • sm))) =
    (dpScalarExtensionEquiv R S M) (r ^ n • (dpScalarExtensionEquiv R S M).symm (dp S n sm))

State before:
case a
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
sm : S ⊗[R] M
⊢ (dpScalarExtensionEquiv R S M) ((dpScalarExtensionEquiv R S M).symm (dp S n (r • sm))) =
    (dpScalarExtensionEquiv R S M) (r ^ n • (dpScalarExtensionEquiv R S M).symm (dp S n sm))
Tactic:
simp only [apply_symm_apply, LinearMapClass.map_smul]
State after:
case a
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
sm : S ⊗[R] M
⊢ dp S n (r • sm) = r ^ n • dp S n sm

State before:
case a
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
sm : S ⊗[R] M
⊢ dp S n (r • sm) = r ^ n • dp S n sm
Tactic:
rw [dp_smul]
State after:
no goals