feat(MvPowerSeries): add some equivs and lemmas#37633
feat(MvPowerSeries): add some equivs and lemmas#37633WenrongZou wants to merge 19 commits intoleanprover-community:masterfrom
Conversation
github-actions
bot
added
the
large-import
PR summary 7d81886827Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.RingTheory.MvPowerSeries.Rename | 1127 | 1435 | +308 (+27.33%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.RingTheory.MvPowerSeries.Rename |
308 |
Mathlib.RingTheory.MvPowerSeries.Equiv (new file) |
1472 |
Declarations diff
+ C_inj
+ C_injective
+ C_surjective
+ HasSubst.X_comp
+ HasSubst.toMvPowerSeries
+ MvPowerSeries.rename_comp_toMvPowerSeries
+ MvPowerSeries.rename_toMvPowerSeries
+ _root_.MvPowerSeries.monomial_mapDomain_eq_prod
+ mapAlgEquiv
+ mapAlgEquiv_refl
+ mapAlgEquiv_symm
+ mapAlgEquiv_trans
+ mapEquiv
+ mapEquiv_refl
+ mapEquiv_symm
+ mapEquiv_trans
+ map_injective
+ map_injective_iff
+ map_leftInverse
+ map_rightInverse
+ map_surjective
+ map_surjective_iff
+ rename_eq_subst
+ toMvPowerSeries
+ toMvPowerSeries_C
+ toMvPowerSeries_X
+ toMvPowerSeries_apply
+ toMvPowerSeries_eq_subst
+ toMvPowerSeries_injective
+ toMvPowerSeries_val
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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
1 participant
In this PR, I add some basic equivalences between multivariate power series.