Commit 2026-09-10 16:50 1192d624

refactor: make several definitions take concrete morphism classes (#43596) Specifically, this PR changes NonUnitalSubring.{map,comap,equivMapOfInjective} as well as NonUnitalSubsemiring.{map,comap,srangeRestrict,sofLeftInverse'}, and adapts all theorems about them to take in a concrete morphism also. Since this removes all uses of a bundled morphism class, we also remove the assocated variable lines and align them with standard mathlib style. This follows the general patterns established in https://github.com/leanprover-community/mathlib4/issues/31365:

we should restrict definitions to explicit morphisms, instead of morphism classes in order to avoid proliferating definitions. Given a definition Bar that takes FooHom as an argument, a theorem whose statement involves Bar should only ever be written for FooHoms and never FooHomClasses. Indeed in the latter case, the statement would require the coercion from the morphism class to the morphism, thereby making it less general.