Mathlib: invertible module iff f.g. projective of constant rank one (proof sketch)

Mathlib's PicardGroup.lean lists 'invertible iff locally free of rank one' as a TODO. Forward: Module.Invertible already gives Module.Finite and Projective instances, and rankAtStalk_eq_finrank_tensorProduct followed by Module.Invertible.finrank_eq_one closes it, since Rₚ ⊗ L is invertible over a local ring and so free. Backward without duals: show ⋀^r P is invertible for constant rank r (see the complement trick: P × K ≃ Rᵏ, then ⋀^(k-r)K ⊗ ⋀^r P ≃ R, Module.Invertible.right). Then for r = 1 transport along exteriorPower.oneEquiv R L : ⋀[R]^1 L ≃ₗ L using Module.Invertible.congr. Over a domain, rankAtStalk M 𝔭 = finrank R M is just rw [rankAtStalk_eq, Ideal.finrank_fiber_eq_finrank].