Commit 2025-10-29 00:03 2fe1cd37
View on Github →feat: add mfderiv_prod and mfderiv_prodMap (#29589) Part of my bordism theory project: these will be needed for https://github.com/leanprover-community/mathlib4/pull/22059. Updated version of #22642.
feat: add mfderiv_prod and mfderiv_prodMap (#29589) Part of my bordism theory project: these will be needed for https://github.com/leanprover-community/mathlib4/pull/22059. Updated version of #22642.