Mathlib Changelog
v4
Changelog
About
Github
Theorem
LinearMap.isBigOTVS_rev_comp
Modification history
2025-11-25 10:20
Mathlib/Analysis/Asymptotics/TVS.lean
feat(Calculus): derivative of `ContinuousAlternatingMap.compContinuousLinearMap` (#30331)
Added
LinearMap.isBigOTVS_rev_comp
View on Github →