Commit 2026-08-10 08:17 b8d43c43

chore(Order/CompleteBooleanAlgebra): use to_dual (#41792) This PR uses to_dual in Mathlib/Order/CompleteBooleanAlgebra.

• Frame.mk and Coframe.mk are annoyingly not dual to eachother due to the way in which GeneralizedHeytingAlgebra and GeneralizedCoheytingAlgebra are not dual to eachother.
• The MinimalAxioms structures have been refactored into a more natural form. Firstly, they should not be classes since they should not be used in type class search. Additionally, instead of extending CompleteLattice, they now take it as a parameter, so that we can easily talk about the order operations. As a result, the MinimalAxioms structures live in Prop. Some lemmas about MinimalAxioms have been marked private, since these are not meant to be used anywhere else.