Commit 2026-08-25 15:04 c404bb7e

View on Github →

chore(Analysis/Normed): move normSeminorm into new file (#42887) Aims to untangle NormedSpace and Seminorm. We also add checks for GroupSeminorm not importing SeminormedGroup and Seminorm not importing NormedSpace. Copyright goes to Yael for [#11487](https://github.com/leanprover-community/mathlib3/pull/11487) (mathlib3) and Anatole for #5501.

Estimated changes

deleted theorem absorbent_ball
deleted theorem absorbent_ball_zero
deleted theorem balanced_ball_zero
deleted theorem balanced_closedBall_zero
deleted theorem ball_normSeminorm
deleted theorem closedBall_normSeminorm
deleted theorem coe_normSeminorm
deleted def normSeminorm
deleted theorem rescale_to_shell
deleted theorem rescale_to_shell_zpow
added theorem absorbent_ball
added theorem absorbent_ball_zero
added theorem balanced_ball_zero
added theorem ball_normSeminorm
added theorem coe_normSeminorm
added def normSeminorm
added theorem rescale_to_shell
added theorem rescale_to_shell_zpow