mathlib
a4ae4adb - chore(order/(bounded,modular)_lattice): avoid classical.some in `is_complemented` instances (#7814)

Commit

4 years ago

chore(order/(bounded,modular)_lattice): avoid classical.some in `is_complemented` instances (#7814) There's no reason to use it here.

Author

eric-wieser

Parents