Theorem: DividedPowerAlgebra.dp_mem_augIdeal (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
n : ℕ
hn : 0 < n
m : M
⊢ dp R n m ∈ augIdeal R M
Tactic:
rw [mem_augIdeal_iff, dp, algebraMapInv_eq, aeval_X, if_pos hn]
State after:
no goals