a : ℤ
⊢ Associated (↑(natAbs a)) a
a : ℤ
⊢ Ideal.span {↑(natAbs a)} = Ideal.span {a}
rw [Ideal.span_singleton_eq_span_singleton]
no goals
a : ℤ
⊢ Associated (↑(natAbs a)) a
exact (associated_natAbs _).symm