chore: adaptations for nightly-2024-11-15

[kim-em]

No description provided.

[github-actions]

PR summary 3b09f5e448

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Rat.Denumerable	486	485	-1 (-0.21%)
Mathlib.Tactic.NormNum.BigOperators	542	541	-1 (-0.18%)
Mathlib.RingTheory.Algebraic	1359	1358	-1 (-0.07%)
Mathlib.RingTheory.AlgebraicIndependent	1394	1393	-1 (-0.07%)
Mathlib.AlgebraicGeometry.OpenImmersion	1720	1719	-1 (-0.06%)
Mathlib.AlgebraicGeometry.Restrict	1725	1724	-1 (-0.06%)
Mathlib.AlgebraicGeometry.AffineScheme	1775	1774	-1 (-0.06%)
Mathlib.AlgebraicGeometry.Properties	1777	1776	-1 (-0.06%)
Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties	1790	1789	-1 (-0.06%)
Mathlib.AlgebraicGeometry.Noetherian	1798	1797	-1 (-0.06%)
Mathlib.AlgebraicGeometry.SpreadingOut	1817	1816	-1 (-0.06%)
Mathlib.AlgebraicGeometry.RationalMap	1819	1818	-1 (-0.05%)
Mathlib.AlgebraicGeometry.Morphisms.Separated	1950	1949	-1 (-0.05%)

Import changes for all files

Files	Import difference
There are 3650 files with changed transitive imports taking up over 157702 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ getLast_filter'
+ subset_of_le
+ zero
- eraseIdx_insertIdx
- find?_eq_some_iff_getElem
- getElem_insertIdx_of_lt
- getElem_insertIdx_self
- getLast_filter
- getLast_ofFn
- head_ofFn
- insertIdx_comm
- insertIdx_eraseIdx_of_ge
- insertIdx_eraseIdx_of_le
- insertIdx_length_self
- insertIdx_of_length_lt
- insertIdx_succ_cons
- insertIdx_succ_nil
- insertIdx_zero
- length_insertIdx
- length_insertIdx_le_succ
- length_le_length_insertIdx
- mapIdxGo_append
- mem_insertIdx
- modifyNthTail_modifyNthTail
- modifyTailIdx_modifyTailIdx
- modifyTailIdx_modifyTailIdx_le
- modifyTailIdx_modifyTailIdx_same
- ofFn_eq_nil_iff
- ofFn_succ
- ofFn_zero

You can run this locally as follows

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

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

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

---

Increase in tech debt: (relative, absolute) = (5.35, 0.44)

Current number	Change	Type
5085	-11	porting notes
198	13	adaptation notes
224	4	disabled simpNF lints
1554	-2	erw
14	5	maxHeartBeats modifications

Current commit 3b09f5e448
Reference commit 38affacc35

You can run this locally as

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