Theorem OrderedFinpartition.norm_compAlongOrderedFinpartitionL_le

Modification history

2024-12-12 18:27
Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
feat(FaaDiBruno): add `norm_compAlongOrderedFinpartitionL_le` (#19713)
Added OrderedFinpartition.norm_compAlongOrderedFinpartitionL_leView on Github →