draft: semialghom

[smmercuri]

---

[github-actions]

PR summary cc9c9b7838

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ AlgEquiv.mk'
+ AlgHomClass.commutes
+ AlgHomClass.map_smul
+ SemialgEquivClass
+ SemialgHom
+ SemialgHomClass
+ instFunLike
+ instance (priority := 100) : SemialgHomClass F φ A B where __ := ‹SemialgEquivClass F φ A B›
+ instance : CoeHead F (A ≃ₛₐ[φ] B) where coe f := semialgEquiv f
+ instance : CoeOut (A₁ ≃ₛₐ[φ] A₂) (A₁ ≃+* A₂) where coe := AlgEquiv.toRingEquiv
+ instance : CoeTC F (A →ₛₐ[φ] B)
+ instance : EquivLike (A₁ ≃ₛₐ[φ] A₂) A₁ A₂
+ instance : FunLike (A₁ ≃ₛₐ[φ] A₂) A₁ A₂
+ instance : Inhabited (A₁ ≃ₐ[R₁] A₁)
+ instance : MulDistribMulAction (A₁ ≃ₐ[R₁] A₁) A₁ˣ
+ instance : SemialgEquivClass (A₁ ≃ₛₐ[φ] A₂) φ A₁ A₂
+ instance _root_.Finite.algEquiv [Finite (A₁ →ₛₐ[φ] A₂)] : Finite (A₁ ≃ₛₐ[φ] A₂)
+ semialgEquiv
+ semialgHom
+ semialgHomClas
++--+ commutes
+--+ congr_arg
- algHomClass
- funLike
- instance (priority := 100) linearMapClass [AlgHomClass F R A B] : LinearMapClass F R A B
- instance : AlgEquivClass (A₁ ≃ₐ[R] A₂) R A₁ A₂
- instance : CoeOut (A₁ ≃ₐ[R] A₂) (A₁ ≃+* A₂) where coe := AlgEquiv.toRingEquiv
- instance : EquivLike (A₁ ≃ₐ[R] A₂) A₁ A₂
- instance : FunLike (A₁ ≃ₐ[R] A₂) A₁ A₂
- instance : Inhabited (A₁ ≃ₐ[R] A₁)
- instance : MulDistribMulAction (A₁ ≃ₐ[R] A₁) A₁ˣ
- instance _root_.Finite.algEquiv [Finite (A₁ →ₐ[R] A₂)] : Finite (A₁ ≃ₐ[R] A₂)
- instance {φ₁ : B →ₐ[R] C} {φ₂ : A →ₐ[R] B} :
- toLinearEquiv
-++- Simps.apply
-++- congr_fun
-++- ext
-++- lift
-+-+ algebraMap_eq_apply
-+-+ coe_coe
-+-+ mk_coe
--+ toLinearMap

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.

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.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).

[github-actions]

🚨 PR Title Needs Formatting

Please update the title to match our commit style conventions.

Errors from script:

error: the PR title should be of the form
  kind: main title
or
  kind(scope): main title
Allowed values for `kind` are [feat, chore, perf, refactor, style, fix, doc, test, ci]

Details on the required title format

The title should fit the following format:

<kind>(<optional-scope>): <subject>

<kind> is:

• feat (feature)
• fix (bug fix)
• doc (documentation)
• style (formatting, missing semicolons, ...)
• refactor
• test (when adding missing tests)
• chore (maintain)
• perf (performance improvement, optimization, ...)
• ci (changes to continuous integration, repo automation, ...)

<optional-scope> is a name of module or a directory which contains changed modules.
This is not necessary to include, but may be useful if the <subject> is insufficient.
The Mathlib directory prefix is always omitted.
For instance, it could be

• Data/Nat/Basic
• Algebra/Group/Defs
• Topology/Constructions

<subject> has the following constraints:

• do not capitalize the first letter
• no dot(.) at the end
• use imperative, present tense: "change" not "changed" nor "changes"