chore: rename CoAlg{Hom,Equiv}Class.toCoAlg{Hom,Equiv} as CoAlg{Hom,Equiv}.ofClass

[grunweg]

and rename affected lemmas accordingly.

Following item (2) in #31365, the definition which implements the coercion from a morphism class FooHomClass to FooHoms should be called FooHom.ofClass.

This makes two more classes follow this pattern.

---

• depends on: chore: rename Alg{Hom,Equiv}Class.toAlg{Hom,Equiv} to Alg{Hom,Equiv}.ofClass #43557

[mathlib-dependent-issues]

This PR/issue depends on:

• chore: rename Alg{Hom,Equiv}Class.toAlg{Hom,Equiv} to Alg{Hom,Equiv}.ofClass #43557
  By Dependent Issues (🤖). Happy coding!

[github-actions]

PR summary 2465fae17f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ _root_.AlgEquiv.ofClass
+ _root_.AlgHom.ofClass
+ _root_.AlgHomClass.linearMapOfClass_ofClass
+ _root_.CoAlgHom.ofClass
+ _root_.CoalgEquiv.ofClass
+ apply_ofClass_symm_apply
+ coe_coAlgHomOfClass
+ coe_linearMapOfClass
+ linearMapOfClass_injective
+ ofClass_symm_apply_apply
+ toCoAlgHom
+ toCoalgHom_eq_ofClass
+ toLinearMap_eq_ofClass
+ toRingHom_ofClass
++++ coe_ofClass
++++---- coe_coe
- _root_.AlgHomClass.toLinearMap_toAlgHom
- toCoalgHom

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 2465fae17f
Reference commit 38f65a093a

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).