feat(IsGaloisGroup): add restrictHom

[xroblot]

---

[github-actions]

PR summary 92b003b91b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ IsGaloisGroup.of_algEquiv
+ IsGaloisGroup.of_ringEquiv
+ IsGaloisGroup.smul_eq_self
+ _root_.MulEquiv.mapSubgroup_normal_iff
+ algebraMap_quotientMulEquiv_smul
+ algebraMap_restrictHom_smul
+ algebraMap_smulOfNormal
+ coe_smul_smulQuotient
+ equivFieldRange
+ equivFieldRange_apply
+ faithfulSMul
+ fixingSubgroup_range_algebraMap
+ fixingSubgroup_range_algebraMap'
+ fixingSubgroup_range_algebraMap_isFractionRing
+ instIsGaloisGroupQuotient
+ instMulSemiringActionQuotient
+ instance [SMulCommClass G K L] [MulSemiringAction G F] [SMulDistribClass G F L]
+ isGaloisGroup_fixingSubgroup_range_algebraMap
+ isInvariant
+ isScalarTower_smulQuotient
+ map_quotientMk'
+ mulActionQuotient
+ mulEquivCongr'
+ mulEquivCongr'_apply_smul
+ mulEquivCongr_mapSubgroup_fixingSubgroup
+ mulEquivCongr_symm_apply_smul
+ mulSemiringAction
+ mulSemiringAction_of_smulDistribClass
+ normal_of_isGalois
+ normal_of_isGaloisGroup
+ of_isScalarTower
+ quotientMulEquiv
+ restrictHom
+ smulCommClass
+ smulCommClassQuotient
+ smulDistribClass
+ smulDistribClass_smulOfNormal
+ smulOfNormal
+ smulQuotient
- instance [SMulCommClass G K L] : SMulCommClass (G ⧸ N) K F
- smul_eq_self

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.

---

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