Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-18 14:10 9a302352

View on Github →

chore(data/polynomial): move auxiliary definitions/theorems to appropriate places

Estimated changes

Modified algebra/ordered_group.lean

added theorem with_bot.add_bot

added theorem with_bot.bot_add

added theorem with_bot.bot_lt_some

added theorem with_bot.coe_add

added theorem with_bot.coe_lt_coe

Modified algebra/ring.lean

Modified data/finsupp.lean

added theorem finsupp.mul_sum

added theorem finsupp.sum_mul

Modified data/polynomial.lean

deleted theorem finsupp.mul_sum

deleted theorem finsupp.sum_mul

deleted theorem with_bot.add_bot

deleted theorem with_bot.bot_add

deleted theorem with_bot.bot_lt_some

deleted theorem with_bot.coe_add

deleted theorem with_bot.coe_lt_coe