Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-23 14:59 ea665e7d

View on Github →

fix(algebra/ordered*): add norm_cast attribute (#3132)

Estimated changes

Modified src/algebra/group_power.lean

Modified src/algebra/ordered_group.lean

modified theorem with_bot.coe_add

added theorem with_bot.coe_bit0

added theorem with_bot.coe_bit1

added theorem with_bot.coe_eq_zero

modified theorem with_bot.coe_one

modified theorem with_bot.coe_zero

modified theorem with_top.coe_add

added theorem with_top.coe_bit0

added theorem with_top.coe_bit1

added theorem with_top.coe_eq_one

added theorem with_top.coe_eq_zero

added theorem with_top.coe_one

added theorem with_top.coe_zero

modified theorem with_top.zero_lt_coe

Modified src/algebra/ordered_ring.lean

deleted theorem with_top.coe_eq_zero

deleted theorem with_top.coe_zero

Modified src/order/bounded_lattice.lean

modified theorem with_bot.coe_le_coe

modified theorem with_top.coe_le_coe

Modified src/ring_theory/unique_factorization_domain.lean