In this patch we create a new file Basics/Classes.v which contain some basic classes. In the future we will move some more stuff from canonical_names.v and abstract_algebra.v here that should be more widely available.
For now we introduce the IsInjective predicate more generally for everybody to use and adapt existing proofs to use this.
In this patch we create a new file Basics/Classes.v which contain some basic classes. In the future we will move some more stuff from canonical_names.v and abstract_algebra.v here that should be more widely available.
For now we introduce the IsInjective predicate more generally for everybody to use and adapt existing proofs to use this.