Commit 2021-09-14 06:36 ceab0e7f

View on Github →

chore(order/bounded_lattice): make bot_lt_some and some_lt_none consistent (#9180) with_bot.bot_lt_some gets renamed to with_bot.none_lt_some and now syntactically applies to none : with_bot α (with_bot.bot_le_coe already applies to ⊥ and ↑a). with_top.some_lt_none now takes a explicit.

Estimated changes

Modified src/data/nat/with_bot.lean

Modified src/data/polynomial/degree/definitions.lean

Modified src/data/polynomial/div.lean

Modified src/order/bounded_lattice.lean

modified theorem with_bot.bot_lt_coe

deleted theorem with_bot.bot_lt_some

added theorem with_bot.none_lt_some

modified theorem with_top.coe_lt_top

modified theorem with_top.some_lt_none

Modified src/ring_theory/power_basis.lean