Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-09 13:27 cde6e632

View on Github →

feat(analysis/seminorm): removed unnecessary norm_one_class arguments (#14614)

Estimated changes

Modified src/analysis/seminorm.lean

modified theorem balanced_ball_zero

modified theorem seminorm.le_insert'

modified theorem seminorm.le_insert

modified theorem seminorm.nonneg

modified theorem seminorm.sub_rev