Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-28 17:52 762fc150

View on Github →

feat(set_theory/ordinal/arithmetic): Add missing instances for ordinal (#14128) We add the following instances:

  • monoid_with_zero ordinal
  • no_zero_divisors ordinal
  • is_left_distrib_class ordinal
  • contravariant_class ordinal ordinal (swap (+)) (<)
  • is_antisymm ordinal (∣)

Estimated changes

deleted theorem ordinal.dvd_add
deleted theorem ordinal.dvd_zero
deleted theorem ordinal.mul_add
deleted theorem ordinal.mul_add_one
deleted theorem ordinal.mul_eq_zero_iff
deleted theorem ordinal.mul_one_add
modified theorem ordinal.mul_succ
deleted theorem ordinal.mul_two
deleted theorem ordinal.mul_zero
deleted theorem ordinal.one_dvd
modified theorem ordinal.succ_zero
deleted theorem ordinal.zero_dvd
deleted theorem ordinal.zero_mul
deleted theorem onote.mul_zero
deleted theorem onote.zero_mul