[Merged by Bors] - chore: adaptations for nightly-2024-07-09#14604
Closed
jcommelin wants to merge 3 commits intobump/v4.11.0from
Closed
[Merged by Bors] - chore: adaptations for nightly-2024-07-09#14604jcommelin wants to merge 3 commits intobump/v4.11.0from
jcommelin wants to merge 3 commits intobump/v4.11.0from
Conversation
Member
jcommelin
commented
Jul 10, 2024
PR summary cbaf46b939
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Lean.Name | 3 | 2 | -1 (-33.33%) |
| Mathlib.Tactic.Attr.Core | 5 | 4 | -1 (-20.00%) |
| Mathlib.Util.LongNames | 11 | 9 | -2 (-18.18%) |
| Mathlib.Control.Traversable.Basic | 38 | 37 | -1 (-2.63%) |
| Mathlib.Algebra.Ring.Ext | 113 | 112 | -1 (-0.88%) |
| Mathlib.CategoryTheory.Functor.Category | 259 | 257 | -2 (-0.77%) |
| Mathlib.CategoryTheory.Thin | 260 | 258 | -2 (-0.77%) |
| Mathlib.CategoryTheory.Comma.Basic | 269 | 267 | -2 (-0.74%) |
| Mathlib.CategoryTheory.Quotient | 269 | 267 | -2 (-0.74%) |
| Mathlib.CategoryTheory.Comma.Arrow | 270 | 268 | -2 (-0.74%) |
| Mathlib.CategoryTheory.PathCategory | 272 | 270 | -2 (-0.74%) |
| Mathlib.Data.Sigma.Lex | 140 | 139 | -1 (-0.71%) |
| Mathlib.CategoryTheory.Category.Pointed | 288 | 286 | -2 (-0.69%) |
| Mathlib.CategoryTheory.Category.Bipointed | 289 | 287 | -2 (-0.69%) |
| Mathlib.CategoryTheory.Monad.Basic | 291 | 289 | -2 (-0.69%) |
| Mathlib.CategoryTheory.Category.TwoP | 292 | 290 | -2 (-0.68%) |
| Mathlib.CategoryTheory.Monad.Algebra | 292 | 290 | -2 (-0.68%) |
| Mathlib.Order.BoundedOrder | 170 | 169 | -1 (-0.59%) |
| Mathlib.Data.Sigma.Order | 173 | 172 | -1 (-0.58%) |
| Mathlib.Algebra.Group.Action.Defs | 280 | 279 | -1 (-0.36%) |
| Mathlib.Algebra.Group.Action.Sigma | 281 | 280 | -1 (-0.36%) |
| Mathlib.CategoryTheory.Bicategory.LocallyDiscrete | 296 | 295 | -1 (-0.34%) |
| Mathlib.Algebra.Free | 302 | 301 | -1 (-0.33%) |
| Mathlib.CategoryTheory.Bicategory.Coherence | 302 | 301 | -1 (-0.33%) |
| Mathlib.CategoryTheory.Yoneda | 302 | 301 | -1 (-0.33%) |
| Mathlib.Data.Fin.Basic | 314 | 313 | -1 (-0.32%) |
| Mathlib.Order.Interval.Set.UnorderedInterval | 316 | 315 | -1 (-0.32%) |
| Mathlib.Algebra.Group.Fin | 319 | 318 | -1 (-0.31%) |
| Mathlib.Order.Fin | 321 | 320 | -1 (-0.31%) |
| Mathlib.CategoryTheory.IsConnected | 331 | 330 | -1 (-0.30%) |
| Mathlib.CategoryTheory.ConnectedComponents | 333 | 332 | -1 (-0.30%) |
| Mathlib.Data.List.AList | 341 | 340 | -1 (-0.29%) |
| Mathlib.GroupTheory.Perm.Basic | 345 | 344 | -1 (-0.29%) |
| Mathlib.Algebra.Group.Support | 356 | 355 | -1 (-0.28%) |
| Mathlib.Algebra.Order.Kleene | 362 | 361 | -1 (-0.28%) |
| Mathlib.CategoryTheory.Monoidal.NaturalTransformation | 367 | 366 | -1 (-0.27%) |
| Mathlib.CategoryTheory.Monoidal.Free.Coherence | 369 | 368 | -1 (-0.27%) |
| Mathlib.GroupTheory.Congruence.Basic | 369 | 368 | -1 (-0.27%) |
| Mathlib.SetTheory.ZFC.Basic | 369 | 368 | -1 (-0.27%) |
| Mathlib.CategoryTheory.Category.PartialFun | 370 | 369 | -1 (-0.27%) |
| Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy | 370 | 369 | -1 (-0.27%) |
| Mathlib.Logic.Encodable.Lattice | 370 | 369 | -1 (-0.27%) |
| Mathlib.Algebra.Module.Defs | 378 | 377 | -1 (-0.26%) |
| Mathlib.CategoryTheory.Endofunctor.Algebra | 380 | 379 | -1 (-0.26%) |
| Mathlib.GroupTheory.SemidirectProduct | 381 | 380 | -1 (-0.26%) |
| Mathlib.GroupTheory.GroupAction.Hom | 382 | 381 | -1 (-0.26%) |
| Mathlib.CategoryTheory.Monoidal.Braided.Basic | 385 | 384 | -1 (-0.26%) |
| Mathlib.CategoryTheory.Localization.Resolution | 386 | 385 | -1 (-0.26%) |
| Mathlib.Algebra.Module.LinearMap.Defs | 393 | 392 | -1 (-0.25%) |
| Mathlib.CategoryTheory.Comma.StructuredArrow | 396 | 395 | -1 (-0.25%) |
| Mathlib.CategoryTheory.Grothendieck | 398 | 397 | -1 (-0.25%) |
| Mathlib.Algebra.Star.StarRingHom | 400 | 399 | -1 (-0.25%) |
| Mathlib.CategoryTheory.Comma.Presheaf | 400 | 399 | -1 (-0.25%) |
| Mathlib.CategoryTheory.Sites.Sieves | 403 | 402 | -1 (-0.25%) |
| Mathlib.CategoryTheory.Limits.Shapes.Images | 408 | 407 | -1 (-0.25%) |
| Mathlib.CategoryTheory.Limits.Types | 410 | 409 | -1 (-0.24%) |
| Mathlib.CategoryTheory.Limits.Preserves.Ulift | 413 | 412 | -1 (-0.24%) |
| Mathlib.Algebra.Module.Equiv | 416 | 415 | -1 (-0.24%) |
| Mathlib.Algebra.Homology.ShortComplex.Basic | 417 | 416 | -1 (-0.24%) |
| Mathlib.CategoryTheory.Sites.Pretopology | 418 | 417 | -1 (-0.24%) |
| Mathlib.CategoryTheory.Sites.SheafOfTypes | 422 | 421 | -1 (-0.24%) |
| Mathlib.GroupTheory.Perm.Support | 424 | 423 | -1 (-0.24%) |
| Mathlib.CategoryTheory.Shift.SingleFunctors | 429 | 428 | -1 (-0.23%) |
| Mathlib.CategoryTheory.DifferentialObject | 431 | 430 | -1 (-0.23%) |
| Mathlib.Data.NNRat.Defs | 444 | 443 | -1 (-0.23%) |
| Mathlib.CategoryTheory.Subobject.Basic | 451 | 450 | -1 (-0.22%) |
| Mathlib.Data.Finmap | 451 | 450 | -1 (-0.22%) |
| Mathlib.CategoryTheory.GradedObject.Monoidal | 456 | 455 | -1 (-0.22%) |
| Mathlib.Algebra.CharP.Defs | 459 | 458 | -1 (-0.22%) |
| Mathlib.CategoryTheory.Monoidal.Mon_ | 460 | 459 | -1 (-0.22%) |
| Mathlib.CategoryTheory.Monoidal.CommMon_ | 461 | 460 | -1 (-0.22%) |
| Mathlib.CategoryTheory.Monoidal.Mod_ | 461 | 460 | -1 (-0.22%) |
| Mathlib.CategoryTheory.Monoidal.Comon_ | 463 | 462 | -1 (-0.22%) |
| Mathlib.CategoryTheory.Monoidal.Bimon_ | 464 | 463 | -1 (-0.22%) |
| Mathlib.CategoryTheory.Monoidal.Bimod | 465 | 464 | -1 (-0.22%) |
| Mathlib.Order.Filter.Basic | 483 | 482 | -1 (-0.21%) |
| Mathlib.Combinatorics.SimpleGraph.Basic | 487 | 486 | -1 (-0.21%) |
| Mathlib.Combinatorics.SimpleGraph.Maps | 490 | 489 | -1 (-0.20%) |
| Mathlib.Data.Finsupp.Defs | 491 | 490 | -1 (-0.20%) |
| Mathlib.CategoryTheory.Filtered.Small | 503 | 502 | -1 (-0.20%) |
| Mathlib.Combinatorics.SimpleGraph.Subgraph | 513 | 512 | -1 (-0.19%) |
| Mathlib.MeasureTheory.MeasurableSpace.Defs | 514 | 513 | -1 (-0.19%) |
| Mathlib.RingTheory.HahnSeries.Basic | 514 | 513 | -1 (-0.19%) |
| Mathlib.CategoryTheory.Limits.Shapes.Biproducts | 515 | 514 | -1 (-0.19%) |
| Mathlib.Deprecated.Subgroup | 515 | 514 | -1 (-0.19%) |
| Mathlib.CategoryTheory.Triangulated.Basic | 527 | 526 | -1 (-0.19%) |
| Mathlib.CategoryTheory.GuitartExact.Basic | 528 | 527 | -1 (-0.19%) |
| Mathlib.CategoryTheory.Monad.Coequalizer | 532 | 531 | -1 (-0.19%) |
| Mathlib.CategoryTheory.Monad.Equalizer | 532 | 531 | -1 (-0.19%) |
| Mathlib.CategoryTheory.Dialectica.Basic | 534 | 533 | -1 (-0.19%) |
| Mathlib.GroupTheory.MonoidLocalization | 535 | 534 | -1 (-0.19%) |
| Mathlib.Order.RelSeries | 536 | 535 | -1 (-0.19%) |
| Mathlib.RepresentationTheory.Action.Basic | 538 | 537 | -1 (-0.19%) |
| Mathlib.CategoryTheory.Limits.VanKampen | 539 | 538 | -1 (-0.19%) |
| Mathlib.Data.Complex.Basic | 539 | 538 | -1 (-0.19%) |
| Mathlib.Algebra.Order.Interval.Basic | 565 | 564 | -1 (-0.18%) |
| Mathlib.Topology.Bornology.Basic | 570 | 569 | -1 (-0.18%) |
| Mathlib.ModelTheory.Basic | 578 | 577 | -1 (-0.17%) |
| Mathlib.RingTheory.HahnSeries.Addition | 578 | 577 | -1 (-0.17%) |
| Mathlib.ModelTheory.Semantics | 581 | 580 | -1 (-0.17%) |
| Mathlib.Combinatorics.Enumerative.Partition | 591 | 590 | -1 (-0.17%) |
| Mathlib.LinearAlgebra.Pi | 593 | 592 | -1 (-0.17%) |
| Mathlib.Topology.Basic | 594 | 593 | -1 (-0.17%) |
| Mathlib.Algebra.Lie.Basic | 599 | 598 | -1 (-0.17%) |
| Mathlib.Topology.Constructions | 599 | 598 | -1 (-0.17%) |
| Mathlib.Topology.ContinuousOn | 600 | 599 | -1 (-0.17%) |
| Mathlib.Topology.UniformSpace.Basic | 611 | 610 | -1 (-0.16%) |
| Mathlib.GroupTheory.CoprodI | 612 | 611 | -1 (-0.16%) |
| Mathlib.Topology.ShrinkingLemma | 633 | 632 | -1 (-0.16%) |
| Mathlib.LinearAlgebra.Span | 634 | 633 | -1 (-0.16%) |
| Mathlib.CategoryTheory.Sites.Sheaf | 646 | 645 | -1 (-0.15%) |
| Mathlib.CategoryTheory.Sites.Coverage | 647 | 646 | -1 (-0.15%) |
| Mathlib.CategoryTheory.Sites.Whiskering | 647 | 646 | -1 (-0.15%) |
| Mathlib.CategoryTheory.Sites.Types | 648 | 647 | -1 (-0.15%) |
| Mathlib.CategoryTheory.Sites.Limits | 656 | 655 | -1 (-0.15%) |
| Mathlib.CategoryTheory.Sites.ConcreteSheafification | 660 | 659 | -1 (-0.15%) |
| Mathlib.CategoryTheory.Idempotents.Karoubi | 663 | 662 | -1 (-0.15%) |
| Mathlib.CategoryTheory.Sites.CoverLifting | 665 | 664 | -1 (-0.15%) |
| Mathlib.Combinatorics.Colex | 665 | 664 | -1 (-0.15%) |
| Mathlib.LinearAlgebra.Multilinear.Basic | 678 | 677 | -1 (-0.15%) |
| Mathlib.Algebra.Category.ModuleCat.Basic | 685 | 684 | -1 (-0.15%) |
| Mathlib.Topology.PartialHomeomorph | 685 | 684 | -1 (-0.15%) |
| Mathlib.Topology.LocallyConstant.Basic | 686 | 685 | -1 (-0.15%) |
| Mathlib.CategoryTheory.Sites.DenseSubsite | 687 | 686 | -1 (-0.15%) |
| Mathlib.Algebra.Algebra.Hom | 689 | 688 | -1 (-0.15%) |
| Mathlib.Algebra.Algebra.NonUnitalHom | 691 | 690 | -1 (-0.14%) |
| Mathlib.Algebra.Algebra.Equiv | 692 | 691 | -1 (-0.14%) |
| Mathlib.Algebra.Star.StarAlgHom | 700 | 699 | -1 (-0.14%) |
| Mathlib.AlgebraicTopology.SimplicialObject | 720 | 719 | -1 (-0.14%) |
| Mathlib.Data.Set.Card | 724 | 723 | -1 (-0.14%) |
| Mathlib.Data.NNReal.Basic | 727 | 726 | -1 (-0.14%) |
| Mathlib.Topology.Category.TopCat.OpenNhds | 730 | 729 | -1 (-0.14%) |
| Mathlib.LinearAlgebra.LinearPMap | 733 | 732 | -1 (-0.14%) |
| Mathlib.LinearAlgebra.BilinearForm.Basic | 734 | 733 | -1 (-0.14%) |
| Mathlib.AlgebraicTopology.SimplicialSet | 735 | 734 | -1 (-0.14%) |
| Mathlib.LinearAlgebra.TensorProduct.Tower | 748 | 747 | -1 (-0.13%) |
| Mathlib.LinearAlgebra.AffineSpace.AffineMap | 755 | 754 | -1 (-0.13%) |
| Mathlib.LinearAlgebra.AffineSpace.AffineSubspace | 758 | 757 | -1 (-0.13%) |
| Mathlib.MeasureTheory.Measure.AddContent | 763 | 762 | -1 (-0.13%) |
| Mathlib.RingTheory.Coalgebra.Hom | 763 | 762 | -1 (-0.13%) |
| Mathlib.RingTheory.Coalgebra.Equiv | 764 | 763 | -1 (-0.13%) |
| Mathlib.Geometry.RingedSpace.PresheafedSpace | 766 | 765 | -1 (-0.13%) |
| Mathlib.ModelTheory.ElementaryMaps | 785 | 784 | -1 (-0.13%) |
| Mathlib.GroupTheory.Perm.Cycle.Factors | 810 | 809 | -1 (-0.12%) |
| Mathlib.Topology.Sheaves.Sheaf | 813 | 812 | -1 (-0.12%) |
| Mathlib.CategoryTheory.Sites.Subsheaf | 818 | 817 | -1 (-0.12%) |
| Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits | 823 | 822 | -1 (-0.12%) |
| Mathlib.NumberTheory.MulChar.Basic | 830 | 829 | -1 (-0.12%) |
| Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover | 846 | 845 | -1 (-0.12%) |
| Mathlib.Topology.MetricSpace.Basic | 848 | 847 | -1 (-0.12%) |
| Mathlib.NumberTheory.DirichletCharacter.Basic | 852 | 851 | -1 (-0.12%) |
| Mathlib.Algebra.DirectSum.Module | 864 | 863 | -1 (-0.12%) |
| Mathlib.LinearAlgebra.Alternating.Basic | 871 | 870 | -1 (-0.11%) |
| Mathlib.Algebra.Category.CoalgebraCat.Basic | 872 | 871 | -1 (-0.11%) |
| Mathlib.Geometry.RingedSpace.SheafedSpace | 878 | 877 | -1 (-0.11%) |
| Mathlib.LinearAlgebra.TensorPower | 885 | 884 | -1 (-0.11%) |
| Mathlib.RingTheory.Valuation.Basic | 900 | 899 | -1 (-0.11%) |
| Mathlib.Algebra.MvPolynomial.Basic | 927 | 926 | -1 (-0.11%) |
| Mathlib.LinearAlgebra.AffineSpace.Independent | 943 | 942 | -1 (-0.11%) |
| Mathlib.RingTheory.MvPowerSeries.Basic | 948 | 947 | -1 (-0.11%) |
| Mathlib.Analysis.Convex.SimplicialComplex.Basic | 963 | 962 | -1 (-0.10%) |
| Mathlib.RingTheory.PowerSeries.Basic | 964 | 963 | -1 (-0.10%) |
| Mathlib.RingTheory.PowerSeries.WellKnown | 965 | 964 | -1 (-0.10%) |
| Mathlib.Topology.Algebra.Module.Basic | 972 | 971 | -1 (-0.10%) |
| Mathlib.Topology.Algebra.ContinuousAffineMap | 978 | 977 | -1 (-0.10%) |
| Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv | 980 | 979 | -1 (-0.10%) |
| Mathlib.Topology.Algebra.Module.Multilinear.Basic | 980 | 979 | -1 (-0.10%) |
| Mathlib.Topology.MetricSpace.Dilation | 982 | 981 | -1 (-0.10%) |
| Mathlib.Algebra.Module.Injective | 997 | 996 | -1 (-0.10%) |
| Mathlib.NumberTheory.Zsqrtd.Basic | 1001 | 1000 | -1 (-0.10%) |
| Mathlib.Algebra.Quaternion | 1003 | 1002 | -1 (-0.10%) |
| Mathlib.Topology.Algebra.Module.Alternating.Basic | 1004 | 1003 | -1 (-0.10%) |
| Mathlib.Analysis.Normed.Group.Hom | 1007 | 1006 | -1 (-0.10%) |
| Mathlib.NumberTheory.ArithmeticFunction | 1008 | 1007 | -1 (-0.10%) |
| Mathlib.Algebra.CubicDiscriminant | 1025 | 1024 | -1 (-0.10%) |
| Mathlib.GroupTheory.PushoutI | 1026 | 1025 | -1 (-0.10%) |
| Mathlib.RingTheory.MvPolynomial.Localization | 1029 | 1028 | -1 (-0.10%) |
| Mathlib.Algebra.Homology.HomotopyCategory.HomComplex | 1034 | 1033 | -1 (-0.10%) |
| Mathlib.CategoryTheory.Galois.Prorepresentability | 1044 | 1043 | -1 (-0.10%) |
| Mathlib.RingTheory.AdicCompletion.Basic | 1080 | 1079 | -1 (-0.09%) |
| Mathlib.RingTheory.Filtration | 1087 | 1086 | -1 (-0.09%) |
| Mathlib.NumberTheory.Bernoulli | 1094 | 1093 | -1 (-0.09%) |
| Mathlib.GroupTheory.Sylow | 1096 | 1095 | -1 (-0.09%) |
| Mathlib.RingTheory.IsTensorProduct | 1115 | 1114 | -1 (-0.09%) |
| Mathlib.RingTheory.Bialgebra.Hom | 1118 | 1117 | -1 (-0.09%) |
| Mathlib.RingTheory.Bialgebra.Equiv | 1120 | 1119 | -1 (-0.09%) |
| Mathlib.Analysis.NormedSpace.ENorm | 1141 | 1140 | -1 (-0.09%) |
| Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber | 1147 | 1146 | -1 (-0.09%) |
| Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion | 1148 | 1147 | -1 (-0.09%) |
| Mathlib.Analysis.BoxIntegral.Partition.Filter | 1152 | 1151 | -1 (-0.09%) |
| Mathlib.MeasureTheory.Measure.MeasureSpaceDef | 1156 | 1155 | -1 (-0.09%) |
| Mathlib.LinearAlgebra.Dual | 1162 | 1161 | -1 (-0.09%) |
| Mathlib.LinearAlgebra.BilinearForm.Properties | 1165 | 1164 | -1 (-0.09%) |
| Mathlib.Algebra.Lie.DirectSum | 1170 | 1169 | -1 (-0.09%) |
| Mathlib.Probability.ProbabilityMassFunction.Basic | 1173 | 1172 | -1 (-0.09%) |
| Mathlib.LinearAlgebra.QuadraticForm.Basic | 1183 | 1182 | -1 (-0.08%) |
| Mathlib.LinearAlgebra.Trace | 1185 | 1184 | -1 (-0.08%) |
| Mathlib.LinearAlgebra.Charpoly.Basic | 1188 | 1187 | -1 (-0.08%) |
| Mathlib.MeasureTheory.Measure.Stieltjes | 1190 | 1189 | -1 (-0.08%) |
| Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps | 1193 | 1192 | -1 (-0.08%) |
| Mathlib.LinearAlgebra.CliffordAlgebra.Even | 1200 | 1199 | -1 (-0.08%) |
| Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv | 1203 | 1202 | -1 (-0.08%) |
| Mathlib.RingTheory.WittVector.Defs | 1203 | 1202 | -1 (-0.08%) |
| Mathlib.RingTheory.WittVector.InitTail | 1210 | 1209 | -1 (-0.08%) |
| Mathlib.RingTheory.WittVector.Truncated | 1211 | 1210 | -1 (-0.08%) |
| Mathlib.RingTheory.WittVector.Frobenius | 1224 | 1223 | -1 (-0.08%) |
| Mathlib.Algebra.Category.BialgebraCat.Basic | 1228 | 1227 | -1 (-0.08%) |
| Mathlib.MeasureTheory.Function.AEEqFun | 1240 | 1239 | -1 (-0.08%) |
| Mathlib.Analysis.NormedSpace.Multilinear.Basic | 1249 | 1248 | -1 (-0.08%) |
| Mathlib.MeasureTheory.Decomposition.Jordan | 1249 | 1248 | -1 (-0.08%) |
| Mathlib.Analysis.Calculus.FormalMultilinearSeries | 1251 | 1250 | -1 (-0.08%) |
| Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic | 1255 | 1254 | -1 (-0.08%) |
| Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal | 1258 | 1257 | -1 (-0.08%) |
| Mathlib.Algebra.Lie.Weights.Basic | 1260 | 1259 | -1 (-0.08%) |
| Mathlib.Analysis.NormedSpace.Star.Unitization | 1261 | 1260 | -1 (-0.08%) |
| Mathlib.RingTheory.DedekindDomain.Ideal | 1273 | 1272 | -1 (-0.08%) |
| Mathlib.RingTheory.ClassGroup | 1274 | 1273 | -1 (-0.08%) |
| Mathlib.RingTheory.DedekindDomain.Factorization | 1274 | 1273 | -1 (-0.08%) |
| Mathlib.NumberTheory.NumberField.Basic | 1279 | 1278 | -1 (-0.08%) |
| Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat | 1289 | 1288 | -1 (-0.08%) |
| Mathlib.Analysis.SpecialFunctions.Complex.Arg | 1308 | 1307 | -1 (-0.08%) |
| Mathlib.Analysis.SpecialFunctions.Complex.Log | 1311 | 1310 | -1 (-0.08%) |
| Mathlib.Analysis.NormedSpace.lpSpace | 1346 | 1345 | -1 (-0.07%) |
| Mathlib.RingTheory.LaurentSeries | 1356 | 1355 | -1 (-0.07%) |
| Mathlib.RepresentationTheory.Rep | 1366 | 1365 | -1 (-0.07%) |
| Mathlib.Topology.ContinuousFunction.StoneWeierstrass | 1367 | 1366 | -1 (-0.07%) |
| Mathlib.NumberTheory.Pell | 1374 | 1373 | -1 (-0.07%) |
| Mathlib.Analysis.Complex.UpperHalfPlane.Basic | 1392 | 1391 | -1 (-0.07%) |
| Mathlib.Algebra.Category.ModuleCat.Sheaf | 1409 | 1408 | -1 (-0.07%) |
| Mathlib.Analysis.Complex.Isometry | 1417 | 1416 | -1 (-0.07%) |
| Mathlib.RingTheory.WittVector.Compare | 1423 | 1422 | -1 (-0.07%) |
| Mathlib.Topology.Sheaves.Skyscraper | 1423 | 1422 | -1 (-0.07%) |
| Mathlib.Geometry.RingedSpace.LocallyRingedSpace | 1432 | 1431 | -1 (-0.07%) |
| Mathlib.Geometry.RingedSpace.OpenImmersion | 1433 | 1432 | -1 (-0.07%) |
| Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits | 1436 | 1435 | -1 (-0.07%) |
| Mathlib.Analysis.NormedSpace.Complemented | 1442 | 1441 | -1 (-0.07%) |
| Mathlib.MeasureTheory.Function.LpSpace | 1450 | 1449 | -1 (-0.07%) |
| Mathlib.Analysis.Complex.Conformal | 1505 | 1504 | -1 (-0.07%) |
| Mathlib.Geometry.Manifold.MFDeriv.Basic | 1516 | 1515 | -1 (-0.07%) |
| Mathlib.Geometry.Euclidean.Sphere.Basic | 1525 | 1524 | -1 (-0.07%) |
| Mathlib.AlgebraicGeometry.Spec | 1527 | 1526 | -1 (-0.07%) |
| Mathlib.Geometry.Euclidean.Circumcenter | 1528 | 1527 | -1 (-0.07%) |
| Mathlib.Analysis.Complex.RealDeriv | 1537 | 1536 | -1 (-0.07%) |
| Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme | 1547 | 1546 | -1 (-0.06%) |
| Mathlib.AlgebraicGeometry.Limits | 1555 | 1554 | -1 (-0.06%) |
| Mathlib.NumberTheory.ModularForms.Basic | 1570 | 1569 | -1 (-0.06%) |
| Mathlib.Analysis.Complex.UpperHalfPlane.Metric | 1589 | 1588 | -1 (-0.06%) |
| Mathlib.Probability.Kernel.Basic | 1607 | 1606 | -1 (-0.06%) |
| Mathlib.Geometry.Euclidean.Angle.Sphere | 1654 | 1653 | -1 (-0.06%) |
| Mathlib.MeasureTheory.Measure.Haar.Unique | 1694 | 1693 | -1 (-0.06%) |
| Mathlib.Probability.Kernel.RadonNikodym | 1739 | 1738 | -1 (-0.06%) |
| Mathlib.Analysis.SpecialFunctions.Complex.Arctan | 1773 | 1772 | -1 (-0.06%) |
| Mathlib.Analysis.Complex.Hadamard | 1805 | 1804 | -1 (-0.06%) |
Import changes for all files
| Files | Import difference |
|---|---|
| Too many changes (4007)! |
Declarations diff
+ instance : (forget V G).Faithful where map_injective w := Hom.ext w
+ instance [DecidableEq α] : DecidableEq αˣ := fun _ _ => decidable_of_iff' _ Units.ext_iff
++++ ext_iff'
- AddContent.ext_iff
- Bornology.ext_iff
- MeasurableSpace.ext_iff
- Perm.ext_iff
- eq_iff
- get!_none
- get!_some
- instance : (forget V G).Faithful where map_injective w := Hom.ext _ _ w
- instance [DecidableEq α] : DecidableEq αˣ := fun _ _ => decidable_of_iff' _ ext_iff
- isSome_map
- limit_ext_iff
- pi_ext'_iff
- unique_ext_iff
-++- ext
-+-+ Hom.ext'
-- subtype_ext_iff
--- ext_ring_iff
---------------------------------------------------------------------------------------------------------- ext_iff
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>
Ruben-VandeVelde
approved these changes
Jul 10, 2024
Contributor
Ruben-VandeVelde
left a comment
There was a problem hiding this comment.
Two comments I'd like you to fix before merging (Mathlib/CategoryTheory/Bicategory/Coherence.lean and Mathlib/NumberTheory/Bernoulli.lean).
I think we should try to keep the divergence between master and the bump branches minimal, so I'd like to see use make ext_iff protected on master, and fix the few lemmas that are currently in the wrong direction. That shouldn't block this PR, though, and I can try to make some time to work on that myself as well.
| @[ext] theorem ext {a b : ℍ} (h : (a : ℂ) = b) : a = b := Subtype.eq h | ||
|
|
||
| @[simp, norm_cast] theorem ext_iff {a b : ℍ} : (a : ℂ) = b ↔ a = b := Subtype.coe_inj | ||
| @[simp, norm_cast] theorem ext_iff' {a b : ℍ} : (a : ℂ) = b ↔ a = b := UpperHalfPlane.ext_iff.symm |
Contributor
There was a problem hiding this comment.
We should swap the direction on master
Contributor
There was a problem hiding this comment.
Sorry, I don't understand what you intend by that. We can't swap the direction, as it will break simp.
| /-- A C⋆-algebra over a densely normed field is a regular normed algebra. -/ | ||
| instance CstarRing.instRegularNormedAlgebra : RegularNormedAlgebra 𝕜 E where | ||
| isometry_mul' := AddMonoidHomClass.isometry_of_norm (mul 𝕜 E) fun a => NNReal.eq_iff.mpr <| | ||
| isometry_mul' := AddMonoidHomClass.isometry_of_norm (mul 𝕜 E) fun a => NNReal.eq_iff.mp <| |
Contributor
There was a problem hiding this comment.
This as well, probably
Contributor
There was a problem hiding this comment.
Again, I don't understand. The meaning if eq_iff is changing because of upstream changes. What would we do on master?
Comment on lines
+166
to
+167
| theorem ext_iff' {s t : Finmap β} : s.entries = t.entries ↔ s = t := | ||
| Finmap.ext_iff.symm |
|
|
||
| /-- Iff version of extensionality rule for congruence relations. -/ | ||
| @[to_additive "Iff version of extensionality rule for additive congruence relations."] | ||
| theorem ext_iff {c d : Con M} : (∀ x y, c x y ↔ d x y) ↔ c = d := |
Contributor
There was a problem hiding this comment.
Also could be flipped
Contributor
There was a problem hiding this comment.
Again unsure what you intended here.
Comment on lines
+349
to
350
| theorem ext_iff' (s₁ s₂ : AffineSubspace k P) : (s₁ : Set P) = s₂ ↔ s₁ = s₂ := | ||
| SetLike.ext'_iff.symm |
Contributor
There was a problem hiding this comment.
As above, not sure what change on master you had in mind.
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Contributor
|
bors merge |
Contributor
|
bors p=10 |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jul 15, 2024
Co-authored-by: Kim Morrison <kim@tqft.net>
Contributor
|
Pull request successfully merged into bump/v4.11.0. Build succeeded: |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jul 15, 2024
From @Ruben-VandeVelde's suggestions at #14604. (There may be more to come in a separate PR as I didn't understand all of their suggestions.)
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jul 15, 2024
From @Ruben-VandeVelde's suggestions at #14604. (There may be more to come in a separate PR as I didn't understand all of their suggestions.)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.