mathlib
98c61b1e - feat(order/hom/heyting): Heyting homomorphisms (#15308)

Commit
3 years ago
feat(order/hom/heyting): Heyting homomorphisms (#15308) Define the type of Heyting homomorphisms, maps between Heyting algebras that preserve Heyting implication.
Author
Parents
Loading