Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-11 12:26 fb987e22

View on Github →

chore(analysis/seminorm): golf (#18089) A part of this PR is forward-ported as leanprover-community/mathlib4#1429

Estimated changes

Modified src/algebra/order/field/basic.lean

added theorem exists_pos_lt_mul

Modified src/analysis/locally_convex/abs_convex.lean

Modified src/analysis/locally_convex/bounded.lean

Modified src/analysis/locally_convex/with_seminorms.lean

Modified src/analysis/seminorm.lean

modified theorem seminorm.smul_ball_zero