Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-04 16:45 7d42deda

View on Github →

chore(*): Rename instances (#9200) Rename

  • lattice_of_linear_order -> linear_order.to_lattice
  • distrib_lattice_of_linear_order -> linear_order.to_distrib_lattice to follow the naming convention (well, it's currently not explicitly written there, but autogenerated names follow that).

Estimated changes