Commit 2025-11-26 01:45 483cf36e

View on Github →

feat(DifferentialForm): pullback commutes with exterior derivative (#30871)

Estimated changes

Modified Mathlib/Analysis/Calculus/DifferentialForm/Basic.lean

added theorem extDerivWithin_pullback

added theorem extDeriv_pullback

Modified Mathlib/Analysis/Normed/Module/Alternating/Basic.lean

added theorem ContinuousAlternatingMap.compContinuousLinearMapCLM_apply

added def ContinuousAlternatingMap.fderivCompContinuousLinearMapCLM

added theorem ContinuousAlternatingMap.fderivCompContinuousLinearMapCLM_apply

added theorem ContinuousAlternatingMap.fderivCompContinuousLinearMap_of_isEmpty

Modified Mathlib/Analysis/Normed/Module/Alternating/Uncurry/Fin.lean

added theorem ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply

added theorem ContinuousAlternatingMap.alternatizeUncurryFin_fderivCompContinuousLinearMap_eq_zero

added theorem ContinuousAlternatingMap.fderivCompContinuousLinearMap_eq_alternatizeUncurryFin

Modified Mathlib/Data/Fin/Tuple/Basic.lean

added theorem Fin.removeNth_fun_const

Modified Mathlib/LinearAlgebra/Alternating/Uncurry/Fin.lean