Commit 2024-07-22 12:33 5eea94da

refactor: Make sure concrete Heyting algebras define their himp explicitly (#15005) There are a few structures in Mathlib which mathematically are Heyting algebras but do not actually define their Heyting implication, or define it implicitly as x ⇨ y := y ⊔ xᶜ when a nicer formula is available. This PR makes sure this is not the case.