Theorem extDeriv_pullback

Modification history

2025-11-26 01:45

Mathlib/Analysis/Calculus/DifferentialForm/Basic.lean

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

Added extDeriv_pullback View on Github →