Lean/Mathlib: primary ideals of a PID are 0 and (p^k), short proof

Mathlib (2026) has no classification of primary ideals in a PID. Short proof of I.IsPrimary ↔ I = ⊥ ∨ ∃ p, Irreducible p ∧ ∃ k, 0 < k ∧ I = span {p ^ k}: (⇐) ⊥ via Ideal.isPrime_bot.isPrimary; (p^k) via isPrimary_of_isMaximal_radical, after rw [← Ideal.span_singleton_pow, Ideal.radical_pow (I := span {p}) hk.ne', (PrincipalIdealRing.isMaximal_of_irreducible hp).isPrime.radical] (radical_pow needs I explicit or the rewrite fails to find the pattern). (⇒) write I = span {a} via (IsPrincipalIdealRing.principal I).principal, get an irreducible factor p from WfDvdMonoid.exists_irreducible_factor, split a = p^k * c with p ∤ c using (FiniteMultiplicity.of_not_isUnit hp.not_isUnit ha0).exists_eq_pow_mul_and_not_dvd, then apply Ideal.isPrimary_iff.1 hI |>.2 to p^k * c ∈ span {a}: either a ∣ p^k (then span_singleton_eq_span_singleton.2 (associated_of_dvd_dvd h ⟨c, hc⟩)) or a ∣ c^n, so p ∣ c by hp.prime.dvd_of_dvd_pow, contradiction. Application: indecomposable f.g. modules over a PID ↔ primary ideals via M ↦ Module.annihilator R M (iso-invariant by LinearEquiv.annihilator_eq; Ideal.annihilator_quotient : annihilator R (R ⧸ I) = I; Module.annihilator_eq_bot + infer_instance for R itself; Submodule.quotEquivOfEqBot ⊥ rfl : (R ⧸ ⊥) ≃ₗ R). For a map out of a Quotient-defined type use _root_.Quotient.lift and induction c using _root_.Quotient.inductionOn; transport Finsupp along an Equiv with Finsupp.domCongr (AddEquiv; domLCongr gets stuck on the scalar ring).