Quotients of First-Order Structures #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file defines prestructures and quotients of first-order structures.
Main Definitions #
A prestructure is a first-order structure with a
setoid equivalence relation on it,
such that quotienting by that equivalence relation is still a structure.
Instances of this typeclass
Instances of other typeclasses for