chore: add simp lemma to unfold Algebra.algHom

[kckennylau]

@[simp] lemma Algebra.coe_algHom : ⇑(Algebra.algHom R A B) = algebraMap A B := rfl

---

[github-actions]

PR summary 401ee04251

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ _root_.Algebra.coe_algHom

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh 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).

[acmepjz]

Sorry for being harsh, but I want to emphasis that there is already https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Algebra/Tower.html#IsScalarTower.toAlgHom which is definitionally equal to Algebra.algHom; IsScalarTower.toAlgHom was introduced to mathlib earlier than Algebra.algHom. Your result added is just https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Algebra/Tower.html#IsScalarTower.coe_toAlgHom and is already a simp lemma. If it was me, I will not add Algebra.coe_algHom to mathlib, instead, I'll use IsScalarTower.toAlgHom.

Related discussion: #mathlib4 > duplication: Algebra.algHom = IsScalarTower.toAlgHom
#22912 (comment)

[artie2000]

maybe we should have one of these simp to the other
or yes deprecate

[ocfnash]

I agree with the remarks above.

Instead of adding Algebra.coe_algHom, we should deprecate Algebra.algHom and its API in favour of IsScalarTower.toAlgHom.

[acmepjz]

I've checked that currently in mathlib, (https://github.com/search?q=repo%3Aleanprover-community%2Fmathlib4%20Algebra.algHom&type=code) besides the definition, there are 6 files using Algebra.algHom, in which only one file Mathlib.LinearAlgebra.TensorProduct.Associator does not import IsScalarTower.toAlgHom. There are 2 open PRs (including the current one) mentioning Algebra.algHom.