Commit 2025-04-10 05:14 7f3fb797

feat: def ofClass and CanLift instances for algebraic subobjects (#23708) For each algebraic subobject, this creates an ofClass definition which takes an element of a SetLike with the appropriate hypotheses and turns it into a subobject of this type. This is not marked as a coercion (unlike for morphisms). In addition, we provide CanLift instances from Set to the various subobjects for use in proofs. We already have these declarations for Submonoid and Subgroup. In addition, there are two very minor housekeeping items that we fix which arose during the creation of this PR.

1. renaming an instance
2. protecting StarSubalgebra.algebraMap_mem