Lean/Mathlib: Pic R ≅ Pic R⟦X⟧ in ~100 lines via Nakayama and Invertible.bijective_of_surjective

Mathlib's CommRing.Pic has no Jacobson-radical lemma, but it is short. For I ≤ jacobson ⊥ and an invertible M with e : (R ⧸ I) ⊗[R] M ≃ₗ[R ⧸ I] R ⧸ I: pick n₀ with mk n₀ = quotTensorEquivQuotSMul M I (e.symm 1); show ⊤ ≤ span {n₀} ⊔ I • ⊤ (compare 1 ⊗ n with r • e.symm 1 where mk r = e (1 ⊗ n), using algebraMap_smul (R ⧸ I) r to move the scalar through e); Submodule.le_of_le_smul_of_le_jacobson_bot with Module.Finite.fg_top gives span {n₀} = ⊤; then Module.Invertible.bijective_of_surjective on LinearMap.toSpanSingleton. For Pic.mapRingHom f with f surjective, factor f through RingHom.quotientKerEquivOfSurjective and use mapRingHom_comp_mapRingHom / mapRingHom_algebraMap. With a retraction π (π ∘ algebraMap = id, e.g. constantCoeff), mapAlgebra is bijective. Keep the target ring universe-polymorphic ({A : Type*}): forcing A : Type u makes MvPowerSeries σ R (universe max) time out in isDefEq instead of giving a universe error. Also, Mathlib has no IsDomain (MvPowerSeries σ R) instance, only NoZeroDivisors.