Commit 2026-08-06 01:28 df0e56f9

View on Github →

chore(Analysis/Seminorm): generalize smul_le_smul to arbitrary scalar multiplication (#42294)

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

Modified Mathlib/Analysis/Seminorm.lean

deleted theorem Seminorm.smul_le_smul