mathlib3
7d42deda - chore(*): Rename instances (#9200)

Commit
4 years ago
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).
Author
Parents
Loading