[Merged by Bors] - chore: adaptations for nightly-2024-06-19 #13981
Conversation
PR summary 9ab70318af
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Algebra.Group.Pi.Basic | 94 | 93 | -1 (-1.06%) |
| Mathlib.Data.Matrix.DMatrix | 102 | 101 | -1 (-0.98%) |
| Mathlib.Data.Nat.Defs | 106 | 105 | -1 (-0.94%) |
| Mathlib.Data.List.GetD | 126 | 125 | -1 (-0.79%) |
| Mathlib.Order.Heyting.Basic | 172 | 171 | -1 (-0.58%) |
| Mathlib.Data.Finset.Basic | 378 | 376 | -2 (-0.53%) |
| Mathlib.Data.Finset.Card | 394 | 392 | -2 (-0.51%) |
| Mathlib.Data.Part | 200 | 199 | -1 (-0.50%) |
| Mathlib.Order.CompleteBooleanAlgebra | 230 | 229 | -1 (-0.43%) |
| Mathlib.Data.Multiset.Fintype | 481 | 479 | -2 (-0.42%) |
| Mathlib.Data.List.Basic | 262 | 261 | -1 (-0.38%) |
| Mathlib.Data.List.Infix | 263 | 262 | -1 (-0.38%) |
| Mathlib.RingTheory.HahnSeries.Basic | 546 | 544 | -2 (-0.37%) |
| Mathlib.Order.Filter.Ultrafilter | 566 | 564 | -2 (-0.35%) |
| Mathlib.Data.List.Rotate | 315 | 314 | -1 (-0.32%) |
| Mathlib.CategoryTheory.Sites.Canonical | 631 | 629 | -2 (-0.32%) |
| Mathlib.Data.List.OfFn | 330 | 329 | -1 (-0.30%) |
| Mathlib.Data.List.Iterate | 405 | 404 | -1 (-0.25%) |
| Mathlib.Computability.TuringMachine | 432 | 431 | -1 (-0.23%) |
| Mathlib.CategoryTheory.GradedObject | 435 | 434 | -1 (-0.23%) |
| Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 | 460 | 459 | -1 (-0.22%) |
| Mathlib.Combinatorics.SimpleGraph.Triangle.Basic | 605 | 604 | -1 (-0.17%) |
| Mathlib.Data.DFinsupp.Basic | 615 | 614 | -1 (-0.16%) |
| Mathlib.Data.Nat.Digits | 642 | 641 | -1 (-0.16%) |
| Mathlib.Data.Finsupp.Basic | 665 | 664 | -1 (-0.15%) |
| Mathlib.Data.Finsupp.ToDFinsupp | 677 | 676 | -1 (-0.15%) |
| Mathlib.Topology.UniformSpace.Completion | 683 | 682 | -1 (-0.15%) |
| Mathlib.CategoryTheory.Preadditive.Biproducts | 697 | 696 | -1 (-0.14%) |
| Mathlib.Topology.Algebra.InfiniteSum.Basic | 737 | 736 | -1 (-0.14%) |
| Mathlib.Data.Matrix.Basic | 774 | 773 | -1 (-0.13%) |
| Mathlib.Data.Matrix.PEquiv | 776 | 775 | -1 (-0.13%) |
| Mathlib.GroupTheory.SpecificGroups.Alternating | 819 | 818 | -1 (-0.12%) |
| Mathlib.GroupTheory.Coxeter.Inversion | 885 | 884 | -1 (-0.11%) |
| Mathlib.Topology.Algebra.GroupCompletion | 888 | 887 | -1 (-0.11%) |
| Mathlib.RingTheory.MvPowerSeries.Basic | 928 | 927 | -1 (-0.11%) |
| Mathlib.LinearAlgebra.Matrix.Transvection | 935 | 934 | -1 (-0.11%) |
| Mathlib.Topology.Connected.PathConnected | 1006 | 1005 | -1 (-0.10%) |
| Mathlib.Order.Filter.ENNReal | 1028 | 1027 | -1 (-0.10%) |
| Mathlib.Topology.Instances.EReal | 1031 | 1030 | -1 (-0.10%) |
| Mathlib.LinearAlgebra.Matrix.Adjugate | 1083 | 1082 | -1 (-0.09%) |
| Mathlib.RingTheory.PolynomialAlgebra | 1103 | 1102 | -1 (-0.09%) |
| Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup | 1121 | 1120 | -1 (-0.09%) |
| Mathlib.LinearAlgebra.TensorProduct.Matrix | 1140 | 1139 | -1 (-0.09%) |
| Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff | 1151 | 1150 | -1 (-0.09%) |
| Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating | 1175 | 1174 | -1 (-0.09%) |
| Mathlib.Algebra.Lie.Classical | 1180 | 1179 | -1 (-0.08%) |
| Mathlib.RingTheory.WittVector.Verschiebung | 1184 | 1183 | -1 (-0.08%) |
| Mathlib.MeasureTheory.Constructions.Pi | 1186 | 1185 | -1 (-0.08%) |
| Mathlib.FieldTheory.PrimitiveElement | 1200 | 1199 | -1 (-0.08%) |
| Mathlib.Analysis.Calculus.FormalMultilinearSeries | 1214 | 1213 | -1 (-0.08%) |
| Mathlib.Topology.ContinuousFunction.Bounded | 1226 | 1225 | -1 (-0.08%) |
| Mathlib.Algebra.Category.Ring.Constructions | 1235 | 1234 | -1 (-0.08%) |
| Mathlib.Analysis.Analytic.Composition | 1239 | 1238 | -1 (-0.08%) |
| Mathlib.Topology.ContinuousFunction.Ideals | 1266 | 1265 | -1 (-0.08%) |
| Mathlib.Analysis.Calculus.ContDiff.Bounds | 1301 | 1300 | -1 (-0.08%) |
| Mathlib.Analysis.NormedSpace.PiLp | 1329 | 1328 | -1 (-0.08%) |
| Mathlib.Analysis.Calculus.UniformLimitsDeriv | 1396 | 1395 | -1 (-0.07%) |
| Mathlib.Geometry.Manifold.ContMDiff.Basic | 1458 | 1457 | -1 (-0.07%) |
| Mathlib.Topology.Category.Profinite.Nobeling | 1462 | 1461 | -1 (-0.07%) |
| Mathlib.RepresentationTheory.GroupCohomology.LowDegree | 1516 | 1515 | -1 (-0.07%) |
| Mathlib.Analysis.InnerProductSpace.LinearPMap | 1522 | 1521 | -1 (-0.07%) |
| Mathlib.Geometry.Manifold.Instances.Real | 1533 | 1532 | -1 (-0.07%) |
| Mathlib.MeasureTheory.Integral.Bochner | 1565 | 1564 | -1 (-0.06%) |
| Mathlib.MeasureTheory.Decomposition.Lebesgue | 1616 | 1615 | -1 (-0.06%) |
| Mathlib.MeasureTheory.Decomposition.RadonNikodym | 1621 | 1620 | -1 (-0.06%) |
| Mathlib.Probability.Variance | 1646 | 1645 | -1 (-0.06%) |
| Mathlib.MeasureTheory.Integral.CircleTransform | 1712 | 1711 | -1 (-0.06%) |
| Mathlib.Probability.Distributions.Gaussian | 1794 | 1793 | -1 (-0.06%) |
| Mathlib.NumberTheory.Harmonic.GammaDeriv | 1823 | 1822 | -1 (-0.05%) |
| Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds | 1868 | 1867 | -1 (-0.05%) |
Declarations diff
+ Fin.univ_image_getElem'
+ IsPrefix.getElem
+ Nodup.erase_getElem
+ Nodup.getElem_inj_iff
+ cons_getElem_drop_succ
+ drop_take_succ_eq_cons_getElem
+ drop_take_succ_join_eq_getElem
+ drop_take_succ_join_eq_getElem'
+ filter_map
+ formPerm_apply_getElem
+ formPerm_apply_getElem_length
+ formPerm_apply_getElem_zero
+ formPerm_apply_lt_getElem
+ formPerm_pow_apply_getElem
+ getElem?_enum
+ getElem?_enumFrom
+ getElem?_getD_replicate_default_eq
+ getElem?_getD_singleton_default_eq
+ getElem?_indexOf
+ getElem?_iterate
+ getElem?_length
+ getElem?_ofFn
+ getElem?_pmap
+ getElem?_rotate
+ getElem?_scanl_zero
+ getElem?_zip_eq_some
+ getElem?_zip_with
+ getElem?_zip_with_eq_some
+ getElem_attach
+ getElem_cyclicPermutations
+ getElem_enum
+ getElem_enumFrom
+ getElem_eq_getElem?
+ getElem_finRange
+ getElem_indexOf
+ getElem_inits
+ getElem_insertNth_add_succ
+ getElem_insertNth_of_lt
+ getElem_insertNth_self
+ getElem_iterate
+ getElem_map_rev
+ getElem_ofFn
+ getElem_ofFn_go
+ getElem_permutations'Aux
+ getElem_pmap
+ getElem_reverse
+ getElem_reverse_aux₂
+ getElem_rotate
+ getElem_scanl_zero
+ getElem_set_of_ne
+ getElem_splitWrtComposition
+ getElem_splitWrtComposition'
+ getElem_splitWrtCompositionAux
+ getElem_tails
+ getElem_zip
+ getElem_zipWith
+ getLast?_eq_none
+ indexOf_getElem
+ neg_def
+ nodup_iff_getElem?_ne_getElem?
+ nodup_iff_injective_getElem
+ ofFn_getElem
+ ofFn_getElem_eq_map
+ toOption_eq_none
- Array.heapSort
- Array.toBinaryHeap
- BinaryHeap
- add_one_le_iff
- add_one_pos
- decreaseKey
- empty
- enum_cons
- enum_nil
- ext_get?
- extractMax
- get
- heapifyDown
- heapifyUp
- increaseKey
- insert
- insertExtractMax
- insert_nil
- instance (lt) : EmptyCollection (BinaryHeap α lt) := ⟨empty _⟩
- instance (lt) : Inhabited (BinaryHeap α lt) := ⟨empty _⟩
- join_replicate_nil
- lt_add_one_iff
- map_replicate
- max
- mkHeap
- mul_sub_one
- popMax
- popMaxAux
- replaceMax
- replicate_one
- replicate_zero
- reverse_replicate
- singleton
- size
- size_heapifyDown
- size_heapifyUp
- size_insert
- size_mkHeap
- size_popMax
- size_pos_of_max
- sub_one_mul
- takeWhile_cons
- takeWhile_nil
-+-+ norm_eq_ciSup
You can run this locally as follows
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>
## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>
|
A lot of changes, but none of the changes looks too bad by itself. bors merge |
github-actions
bot
added
ready-to-merge
This contains adaptations for * leanprover/lean4#4481 * leanprover/lean4#4497 * leanprover/lean4#4387 (Thanks to @JovanGerb for these) * leanprover/lean4#4487
|
Pull request successfully merged into bump/v4.10.0. Build succeeded: |
mathlib-bors
bot
changed the title
|
(bors is fine, but not necessary, on non-master branches) |
This contains adaptations for
simpsupport forOfNatinstances that are functions leanprover/lean4#4481isDefEqleanprover/lean4#4387 (Thanks to @JovanGerb for these)List.replicateleanprover/lean4#4487