Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-28 15:19 dddf6ebe

View on Github →

feat(data/fintype/order): More and better instances (#11702) In a fintype, this allows to promote

  • distrib_lattice to complete_distrib_lattice
  • boolean_algebra to complete_boolean_algebra Also strengthen
  • fintype.to_order_bot
  • fintype.to_order_top
  • fintype.to_bounded_order
  • complete_linear_order.to_conditionally_complete_linear_order_bot

Estimated changes

modified def fintype.to_order_bot
modified def fintype.to_order_top