Theorem: DividedPowerAlgebra.proj'_zero_one (DividedPowers/DPAlgebra/Graded/Basic.lean)

State before:
R : Type u_1
M : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : DecidableEq R
inst✝⁸ : DecidableEq M
S : Type u_3
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : DecidableEq S
inst✝³ : DecidableEq N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
⊢ (proj' R M 0) 1 = 1
Tactic:
rw [proj', proj, LinearMap.coe_mk, AddHom.coe_mk, decompose_one]
State after:
R : Type u_1
M : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : DecidableEq R
inst✝⁸ : DecidableEq M
S : Type u_3
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : DecidableEq S
inst✝³ : DecidableEq N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
⊢ 1 0 = 1

State before:
R : Type u_1
M : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : DecidableEq R
inst✝⁸ : DecidableEq M
S : Type u_3
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : DecidableEq S
inst✝³ : DecidableEq N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
⊢ 1 0 = 1
Tactic:
rfl
State after:
no goals