Theorem ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply

Modification history

2025-11-26 01:45
Mathlib/Analysis/Normed/Module/Alternating/Uncurry/Fin.lean
feat(DifferentialForm): pullback commutes with exterior derivative (#30871)
Added ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_applyView on Github →