[Merged by Bors] - chore: remove June 2025 deprecated declarations #33429
Conversation
Parcly-Taxel
added
tech debt
PR summary d198f498c9
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Algebra.GroupWithZero.Int | 141 | 0 | -141 (-100.00%) |
| Mathlib.Deprecated.RingHom | 164 | 0 | -164 (-100.00%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Deprecated.RingHom |
-164 |
Mathlib.Algebra.GroupWithZero.Int |
-141 |
Declarations diff
- AntitoneOn_insert_iff
- Aut.commGroup
- Bundle.ContinuousLinearMap
- CoproductDisjoint.mono_inl
- CoproductDisjoint.mono_inr
- EventuallyMeasurableSpace
- EventuallyMeasurableSpace.measurableSingleton
- EventuallyMeasurableSpace.measurable_le
- FinitaryPreExtensive.sigma_desc_iso
- H0LequivOfIsTrivial_eq_subtype
- H0Map
- H0Map_comp
- H0Map_comp_f
- H0Map_id
- H0Map_id_comp
- H0Map_id_eq_invariantsFunctor_map
- H1Map
- H1Map_comp
- H1Map_id_comp
- H1Map_one
- H1π_comp_H1Map
- H2Map
- H2Map_comp
- H2Map_id
- H2Map_id_comp
- H2π_comp_H2Map
- IsAlgClosed.hasEnoughRootsOfUnity
- IsAlgClosed.isCyclotomicExtension
- IsAlgClosedOfCharZero.isCyclotomicExtension
- IsCycles.induce_supp
- IsMulOneCoboundary
- IsMulOneCocycle
- IsMulTwoCoboundary
- IsMulTwoCocycle
- IsOneCoboundary
- IsOneCocycle
- IsTwoCoboundary
- IsTwoCocycle
- LE.le.eq_iff_not_lt
- LE.le.eq_of_not_gt
- LE.le.eq_or_gt
- LE.le.gt_or_eq
- LE.le.not_lt
- LT.lt.not_le
- LT.lt.not_lt
- MapSubtype.relIso
- MonotoneOn_insert_iff
- Ne.lt_or_lt
- Ne.not_le_or_not_le
- PseudoEMetricSpace.ofSeminormedAddCommGroupCore
- PseudoMetricSpace.ofSeminormedAddCommGroupCore
- PseudoMetricSpace.ofSeminormedAddCommGroupCoreReplaceAll
- PseudoMetricSpace.ofSeminormedAddCommGroupCoreReplaceUniformity
- Quot
- Quot.Rel
- Quot.desc
- Quot.jointly_surjective
- Quot.map_ι
- Quot.ι
- Quot.ι_desc
- SeminormedAddCommGroup.Core
- Types.Quot.Rel.iff_orbitRel
- Types.Quot.equivOrbitRelQuotient
- abs_qsmul
- append
- baseSet_prod
- bihimp_eq_inf_himp_inf
- braiding_inv_tensor_left
- braiding_inv_tensor_right
- braiding_tensor_left
- braiding_tensor_right
- cochainsMap_f_0_comp_zeroCochainsIso
- cochainsMap_f_1_comp_oneCochainsIso
- cochainsMap_f_2_comp_twoCochainsIso
- cochainsMap_f_3_comp_threeCochainsIso
- cochainsMap_id_f_eq_compLeft
- cocyclesMap_comp_isoOneCocycles_hom
- cocyclesMap_comp_isoTwoCocycles_hom
- cocyclesMap_comp_isoZeroCocycles_hom
- codomain_trivial_iff_range_eq_singleton_zero
- coe_extChartAt_transDiffeomorph
- coe_extChartAt_transDiffeomorph_symm
- coe_list_prod
- coe_list_sum
- coe_mapOneCocycles
- coe_mapTwoCocycles
- coe_multiset_prod
- coe_multiset_sum
- coe_sum
- coe_transDiffeomorph
- coe_transDiffeomorph_symm
- coe_zero
- coinvariantsTensorBarResolution
- colimitEquivQuot
- colimitEquivQuot_apply
- colimitEquivQuot_symm_apply
- comp_dOne_eq
- comp_dTwo_eq
- comp_dZero_eq
- completeSpace_of_isCoherentWith
- constFormalMultilinearSeries_apply
- covariance_same
- dOne
- dOne_apply_mem_twoCocycles
- dOne_comp_dTwo
- dTwo
- dZero
- dZeroArrowIso
- dZero_apply_mem_oneCocycles
- dZero_comp_dOne
- dZero_eq_zero
- dZero_ker_eq_invariants
- diagonalHomEquiv_symm_partialProd_succ
- diagonalSucc
- differentiableAt_id'
- differentiable_at_Gamma_nat_add_one
- differentiable_id'
- disj_sum_strictMono_right
- div_le_of_le_mul'
- div_le_self'
- eq_dOne_comp_inv
- eq_dTwo_comp_inv
- eq_dZero_comp_inv
- eq_iff
- eq_iff_not_lt_of_le
- eq_of_ge_of_not_gt
- eq_of_le_of_le
- eq_or_gt_of_le
- eq_zero_of_double_le
- eq_zero_of_le_half
- equiv_add
- equiv_eq_zero_iff
- equiv_neg
- equiv_smul
- equiv_sub
- equiv_symm_add
- equiv_symm_eq_zero_iff
- equiv_symm_neg
- equiv_symm_smul
- equiv_symm_sub
- equiv_symm_zero
- equiv_zero
- eqvGen_quot_rel_of_rel
- eraseIdx_insertIdx
- exists_forall_hasDerivAt_Ioo_eq_of_contDiffAt
- exists_forall_hasDerivWithinAt_Icc_eq
- extChartAt_transDiffeomorph_target
- fOne
- fThree
- fTwo
- fderivWithin_add'
- fderivWithin_const_smul'
- fderivWithin_neg'
- fderivWithin_sub'
- fderiv_add'
- fderiv_const_smul'
- fderiv_neg'
- fderiv_sub'
- filter_disj_union
- flat_algebraMap_iff
- forall_lt_iff_le'
- getVert_eq_support_get?
- graphFunctor_map
- groupCohomology.extIso
- groupCohomology.projectiveResolution
- groupCohomology.resolution
- groupCohomology.resolution.actionDiagonalSucc
- groupCohomology.resolution.actionDiagonalSucc_hom_apply
- groupCohomology.resolution.actionDiagonalSucc_inv_apply
- groupCohomology.resolution.diagonalSucc
- groupCohomology.resolution.diagonalSucc_hom_single
- groupCohomology.resolution.diagonalSucc_inv_single_left
- groupCohomology.resolution.diagonalSucc_inv_single_right
- groupCohomology.resolution.diagonalSucc_inv_single_single
- groupCohomologyπ
- groupCohomologyπ_comp_isoH0_hom
- groupCohomologyπ_comp_isoH1_hom
- groupCohomologyπ_comp_isoH2_hom
- gt_iff_ne
- gt_irrefl
- gt_of_ge_of_gt
- gt_of_gt_of_ge
- gt_or_eq_of_le
- half_le_of_sub_le_half
- hasColimit_iff_small_quot
- iInf_sup_le_sup_sInf
- inf_sSup_le_iSup_inf
- initialMonoClass_of_disjoint_coproducts
- instFunLike
- inv_apply_eq_iff_eq_apply
- isColimit_iff_bijective_desc
- isEmbedding_prodMk
- isInitialOfIsPullbackOfCoproduct
- isInitialOfIsPullbackOfIsCoproduct
- isInitialOfPullbackOfCoproduct
- isInitialOfPullbackOfIsCoproduct
- isMulOneCoboundary_of_isMulOneCocycle_of_aut_to_units
- isoH0
- isoH1
- isoH2
- isoOneCocycles
- isoOneCocycles_hom_comp_i
- isoOneCocycles_inv_comp_iCocycles
- isoTwoCocycles
- isoTwoCocycles_hom_comp_i
- isoTwoCocycles_inv_comp_iCocycles
- isoZeroCocycles
- isoZeroCocycles_hom_comp_subtype
- isoZeroCocycles_inv_comp_iCocycles
- iteratedDerivWithin_neg'
- le_half_of_half_lt_sub
- le_iff_eq
- le_of_forall_lt'
- le_zero_of_zero_ge
- leftUnitor_tensor
- leftUnitor_tensor'
- leftUnitor_tensor''
- linearYonedaObjResolution
- linearization_of
- lt_or_lt
- lt_zero_of_zero_gt
- mapOneCocycles
- mapOneCocycles_comp_i
- mapOneCocycles_one
- mapTwoCocycles
- mapTwoCocycles_comp_i
- map_dvd
- map_eq_comap
- map_inv_of_isMulOneCocycle
- map_inv_of_isOneCocycle
- map_one_fst_of_isMulTwoCocycle
- map_one_fst_of_isTwoCocycle
- map_one_of_isMulOneCocycle
- map_one_of_isOneCocycle
- map_one_snd_of_isMulTwoCocycle
- map_one_snd_of_isTwoCocycle
- mem_bot
- mem_coe
- mem_def
- mem_oneCocycles_def
- mem_oneCocycles_iff
- mem_oneCocycles_of_addMonoidHom
- mem_twoCocycles_def
- mem_twoCocycles_iff
- mem_zero
- merge_isAssociative
- merge_isCommutative
- merge_isId
- merge_isIdempotent
- mk'
- mono_H0Map_of_mono
- mul_left_eq_self_iff
- mul_right_eq_self_iff
- natCast_zmod_eq_zero_iff_dvd
- nhdsWithin_right_sup_nhds_singleton
- not_dvd_iff_between_consec_multiples
- not_dvd_of_between_consec_multiples
- not_gt_iff_eq
- ofMulActionBasis
- ofMulActionBasisAux
- ofMulAction_free
- oneCoboundaries
- oneCoboundaries.coe_mk
- oneCoboundaries.val_eq_coe
- oneCoboundariesOfIsMulOneCoboundary
- oneCoboundariesOfIsOneCoboundary
- oneCoboundariesToOneCocycles
- oneCoboundariesToOneCocycles_apply
- oneCoboundaries_eq_bot_of_isTrivial
- oneCoboundaries_ext
- oneCoboundaries_le_oneCocycles
- oneCochainsIso
- oneCocycles
- oneCocycles.coe_mk
- oneCocycles.dOne_apply
- oneCocycles.val_eq_coe
- oneCocyclesIsoOfIsTrivial
- oneCocyclesOfIsMulOneCocycle
- oneCocyclesOfIsOneCocycle
- oneCocycles_ext
- oneCocycles_map_inv
- oneCocycles_map_mul_of_isTrivial
- oneCocycles_map_one
- opOp_δ
- opOp_ε
- opOp_η
- opOp_μ
- pointed
- pointed_zero
- prod
- prod_apply
- prod_comp_fst
- prod_comp_snd
- prod_disj_sum
- prod_symm
- punitEquiv
- rel_eq_eqvGen_quot_rel
- rel_of_quot_rel
- rightUnitor_tensor
- selfAction
- setIntegral_zero_measure
- setOf_app_iff
- setOf_set
- small_quot_of_hasColimit
- smul_map_inv_sub_map_inv_of_isTwoCocycle
- subsingleton_fin_one
- subsingleton_fin_zero
- subtype_comp_dZero
- sum_disj_sum
- sum_sq_norm_inner
- symm_linear
- symm_toAffineEquiv
- symm_toHomeomorph
- symm_toLinearEquiv
- threeCochainsIso
- toCocycles_comp_isoOneCocycles_hom
- toCocycles_comp_isoTwoCocycles_hom
- toConvexCone_le_iff
- toConvexCone_pointed
- toIsOrderedAddMonoid
- toMeasure_apply_of_finite
- toSeminormedSpace
- traceForm_dualBasis_powerBasis_eq
- transDiffeomorph
- transDiffeomorph_range
- twoCoboundaries
- twoCoboundaries.coe_mk
- twoCoboundaries.val_eq_coe
- twoCoboundariesOfIsMulTwoCoboundary
- twoCoboundariesOfIsTwoCoboundary
- twoCoboundariesToTwoCocycles
- twoCoboundariesToTwoCocycles_apply
- twoCoboundaries_ext
- twoCoboundaries_le_twoCocycles
- twoCochainsIso
- twoCocycles
- twoCocycles.coe_mk
- twoCocycles.dTwo_apply
- twoCocycles.val_eq_coe
- twoCocyclesOfIsMulTwoCocycle
- twoCocyclesOfIsTwoCocycle
- twoCocycles_ext
- twoCocycles_map_one_fst
- twoCocycles_map_one_snd
- twoCocycles_ρ_map_inv_sub_map_inv
- unopUnop_δ
- unopUnop_ε
- unopUnop_η
- unopUnop_μ
- zeroCochainsIso
-- coe_prod
-- forall_in_swap
-- symm_toEquiv
-- zigzag_of_eqvGen_quot_rel
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.
Decrease in tech debt: (relative, absolute) = (1.37, 0.28)
| Current number | Change | Type |
|---|---|---|
| 5 | -1 | Deprecated files |
| 691 | -52 | total LoC in Deprecated files |
Current commit 44d2a6e06f
Reference commit d198f498c9
You can run this locally as
./scripts/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).
note: file Mathlib/Algebra/GroupWithZero/Int.lean was removed.
Please create a follow-up pull request adding a module deprecation. Thanks!
note: file Mathlib/Deprecated/RingHom.lean was removed.
Please create a follow-up pull request adding a module deprecation. Thanks!
github-actions
bot
added
the
file-removed
|
Thanks! |
leanprover-community-mathlib4-bot
added
the
ready-to-merge
The first commit is the result of running ```lean import Mathlib import Archive import Counterexamples #clear_deprecations "2025-06-01" "2025-06-30" really ``` For the two removed files in the second commit I argue that they effectively _were_ `deprecated_module`s on the same day as their last deprecation was added; they consist entirely of deprecated declarations more than 6 months old, so there is no need to add a module deprecation. Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
|
Pull request successfully merged into master. Build succeeded! And happy new year! 🎉 |
mathlib-bors
bot
changed the title
…#33429) The first commit is the result of running ```lean import Mathlib import Archive import Counterexamples #clear_deprecations "2025-06-01" "2025-06-30" really ``` For the two removed files in the second commit I argue that they effectively _were_ `deprecated_module`s on the same day as their last deprecation was added; they consist entirely of deprecated declarations more than 6 months old, so there is no need to add a module deprecation. Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
3 participants
The first commit is the result of running
For the two removed files in the second commit I argue that they effectively were
deprecated_modules on the same day as their last deprecation was added; they consist entirely of deprecated declarations more than 6 months old, so there is no need to add a module deprecation.