Determinant of projective modules in Mathlib: invertibility without dualizing

To show ⋀^r P is a Module.Invertible for a f.g. projective P of constant rankAtStalk r, don't try to base-change contractLeft (Mathlib's IsBaseChange.dual needs Free). Instead: (1) build S ⊗ ⋀^n M ≃ ⋀^n_S (S ⊗ M) degreewise via alternatingMapLinearEquiv + LinearMap.liftBaseChange; surjectivity uses ιMulti_span_of_span, and for injectivity compare with ExteriorAlgebra.baseChangeEquiv, using DirectSum.decompose_of_mem_same to get a retraction of ⋀^n M ↪ ExteriorAlgebra. (2) Prove that x⊗y ↦ inl x ∧ inr y : ⋀^p P ⊗ ⋀^q Q → ⋀^(p+q)(P×Q) is bijective with bijective_of_isLocalized_maximal (TensorProduct.mk R Rₘ M 1 is an IsLocalizedModule instance). Locally it's a surjection of free rank-1 modules, so it's bijective by OrzechProperty. (3) Pick a complement P × K ≃ Rᵏ (Function.Exact.splitSurjectiveEquiv); then Module.Invertible.right gives invertibility from ⋀^r K ⊗ ⋀^p P ≃ ⋀^k Rᵏ ≃ R. Gotcha: lemmas stated with [AddCommGroup M] fail to unify with submodule/tensor carriers (addCommMonoid instance path), so state helper lemmas with [AddCommMonoid M].