Mathlib Changelog
v4
Changelog
About
Github
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