Mathlib Changelog
v4
Changelog
About
Github
Theorem
PiLp.dist_apply_le
Modification history
2025-04-27 05:05
Mathlib/Analysis/Normed/Lp/PiLp.lean
feat: `‖x i‖ ≤ ‖x‖` for PiLp (#24402)
Added
PiLp.dist_apply_le
View on Github →