mathlib
3838b0e0 - refactor(order/boolean_algebra): Get rid of `boolean_algebra.core` (#15302)

Commit
3 years ago
refactor(order/boolean_algebra): Get rid of `boolean_algebra.core` (#15302) The current setup is problematic for two reasons: * `boolean_algebra.core` is part of the typeclass hierarchy even though it is mathematically the same as `boolean_algebra`. * `boolean_algebra` contains the redundant fields `sup_inf_sdiff` and `inf_inf_sdiff`. The easiest fix is to respectively: * delete `boolean_algebra.core` and use default values in the `boolean_algebra` fields. * not make `boolean_algebra` extend `generalized_boolean_algebra` but instead manually provide the forgetful instance.
Author
Parents
Loading