Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-23 19:11 3362b1e2

View on Github →

refactor(analysis/seminorm): Weaken typeclasses (#10999) This weakens normed_field to the appropriate normed_whatever.

Estimated changes

modified theorem balanced.add
modified theorem balanced.inter
modified theorem balanced.smul_eq
modified theorem balanced.subset_smul
modified theorem balanced.union
modified theorem balanced.univ
modified theorem seminorm.balanced_ball_zero
modified def seminorm.ball
modified theorem seminorm.ball_zero_eq
modified theorem seminorm.mem_ball
modified theorem seminorm.mem_ball_zero
modified theorem seminorm.sub_rev
modified structure seminorm