Commit 2024-08-26 10:46 cf2e934a
View on Github →feat: generalise LinearEquiv.curry to R-modules (#16123)
Generalise statement of LinearEquiv.curry from (ι × κ) → R ≃ₗ[R] ι → κ → R to (ι × κ) → M ≃ₗ[R] ι → κ → M with M an R-module.
feat: generalise LinearEquiv.curry to R-modules (#16123)
Generalise statement of LinearEquiv.curry from (ι × κ) → R ≃ₗ[R] ι → κ → R to (ι × κ) → M ≃ₗ[R] ι → κ → M with M an R-module.