Commit 2026-09-30 15:24 6f454283

feat: in characteristic 0, precomposition by a linear map is analytic on the space of alternating maps (#43338) This is the main missing ingredient to show that the bundle of alternating maps between C^n vector bundles is C^n, in #43234. I was surprised to see that I need characteristic 0 (I could also do the proof in positive characteristic for finite-dimensional T2 spaces, but not in general -- not included in this PR, because the characteristic 0 is the one that interests me). I was afraid I was missing something stupid, then I checked Bourbaki and they have the same condition so it's probably reasonable after all.