Theorem: DividedPowerAlgebra.algebraMap_mem_grade_zero (DividedPowers/DPAlgebra/Graded/GradeZero.lean)

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ (algebraMap R (DividedPowerAlgebra R M)) r ∈ grade R M 0
Tactic:
rw [mem_grade_iff]
State after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ ∃ p ∈ weightedHomogeneousSubmodule R Prod.fst 0, mk p = (algebraMap R (DividedPowerAlgebra R M)) r

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ ∃ p ∈ weightedHomogeneousSubmodule R Prod.fst 0, mk p = (algebraMap R (DividedPowerAlgebra R M)) r
Tactic:
use C r
State after:
case h
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ C r ∈ weightedHomogeneousSubmodule R Prod.fst 0 ∧ mk (C r) = (algebraMap R (DividedPowerAlgebra R M)) r

State before:
case h
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ C r ∈ weightedHomogeneousSubmodule R Prod.fst 0 ∧ mk (C r) = (algebraMap R (DividedPowerAlgebra R M)) r
Tactic:
constructor
State after:
case h.left
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ C r ∈ weightedHomogeneousSubmodule R Prod.fst 0

case h.right
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ mk (C r) = (algebraMap R (DividedPowerAlgebra R M)) r

State before:
case h.left
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ C r ∈ weightedHomogeneousSubmodule R Prod.fst 0
Tactic:
simp only [mem_weightedHomogeneousSubmodule]
State after:
case h.left
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ IsWeightedHomogeneous Prod.fst (C r) 0

State before:
case h.left
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ IsWeightedHomogeneous Prod.fst (C r) 0
Tactic:
exact isWeightedHomogeneous_C Prod.fst r
State after:
no goals

State before:
case h.right
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ mk (C r) = (algebraMap R (DividedPowerAlgebra R M)) r
Tactic:
rw [mk_C]
State after:
no goals