mathlib3

24b08ce6 - feat(order/heyting/regular): Heyting-regular elements (#16033)

feat(order/heyting/regular): Heyting-regular elements (#16033) Define Heyting-regular elements of an Heyting lattice, namely those `a` such that `aᶜᶜ = a`, and prove that they form a boolean algebra.