Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-02-03 23:11
ea1575fd
View on Github →
chore(Analysis/SchwartzSpace): make some definitions private (
#34552
)
Estimated changes
Modified
Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean
deleted
theorem
SchwartzMap.bounds_bddBelow
deleted
theorem
SchwartzMap.bounds_nonempty
deleted
theorem
SchwartzMap.decay_add_le_aux
deleted
theorem
SchwartzMap.decay_neg_aux
deleted
theorem
SchwartzMap.decay_smul_aux
deleted
theorem
SchwartzMap.le_seminormAux
deleted
theorem
SchwartzMap.seminormAux_add_le
deleted
theorem
SchwartzMap.seminormAux_le_bound
deleted
theorem
SchwartzMap.seminormAux_nonneg
deleted
theorem
SchwartzMap.seminormAux_smul_le
deleted
theorem
SchwartzMap.seminormAux_zero
added
theorem
SchwartzMap.seminorm_apply