Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-07 09:39 a7f0069c

View on Github →

chore(algebra/ring): fix docs, def/lemma (#2972)

Estimated changes

Modified src/algebra/ring.lean

deleted def add_mul

deleted def mul_add

deleted def mul_sub

deleted def sub_mul

Modified src/analysis/normed_space/basic.lean

modified theorem norm_tsum_le_tsum_norm