Theorem: DividedPowerAlgebra.mem_augIdeal_iff (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
f : DividedPowerAlgebra R M
⊢ f ∈ augIdeal R M ↔ (algebraMapInv R M) f = 0
Tactic:
rw [augIdeal, RingHom.mem_ker]
State after:
no goals