chore: adaptations for nightly-2025-04-16#24202
Merged
kmill merged 5965 commits intobump/v4.20.0from Apr 19, 2025
Merged
Conversation
…community/mathlib4 into lean-pr-testing-7499
PR summary b460494b92
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Logic.Equiv.Fin.Basic | 364 | 350 | -14 (-3.85%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Data.UInt |
-483 |
Mathlib.Algebra.Expr |
-40 |
Mathlib.Data.Num.Basic |
-36 |
Mathlib.Data.Tree.Get |
-34 |
Mathlib.Algebra.NeZero |
-29 |
Mathlib.Algebra.Order.ZeroLEOne |
-23 |
Mathlib.Data.PNat.Defs Mathlib.Testing.Plausible.Sampleable |
-20 |
9 filesMathlib.Data.PNat.Equiv Mathlib.Data.Set.Insert Mathlib.Data.Set.Subsingleton Mathlib.Logic.Function.FiberPartition Mathlib.Order.Bounded Mathlib.Order.Filter.Defs Mathlib.Order.Interval.Set.Basic Mathlib.Order.Interval.Set.LinearOrder Mathlib.SetTheory.PGame.Basic |
-16 |
78 filesMathlib.Combinatorics.Quiver.Arborescence Mathlib.Data.Bool.Set Mathlib.Data.Countable.Small Mathlib.Data.Nat.Set Mathlib.Data.Rel Mathlib.Data.Semiquot Mathlib.Data.Set.Accumulate Mathlib.Data.Set.BooleanAlgebra Mathlib.Data.Set.Function Mathlib.Data.Set.Functor Mathlib.Data.Set.Image Mathlib.Data.Set.Lattice.Image Mathlib.Data.Set.Lattice Mathlib.Data.Set.List Mathlib.Data.Set.Monotone Mathlib.Data.Set.NAry Mathlib.Data.Set.Pairwise.Basic Mathlib.Data.Set.Pairwise.Lattice Mathlib.Data.Set.Piecewise Mathlib.Data.Set.Prod Mathlib.Data.Set.Restrict Mathlib.Data.Set.Sigma Mathlib.Data.Set.Subset Mathlib.Data.Set.UnionLift Mathlib.Data.Setoid.Basic Mathlib.Logic.Embedding.Set Mathlib.Logic.Equiv.Embedding Mathlib.Logic.Equiv.PartialEquiv Mathlib.Logic.Equiv.Set Mathlib.Logic.Function.DependsOn Mathlib.Logic.Small.Basic Mathlib.Logic.Small.Set Mathlib.Order.Antichain Mathlib.Order.Bounds.Basic Mathlib.Order.Bounds.Image Mathlib.Order.Bounds.Lattice Mathlib.Order.Bounds.OrderIso Mathlib.Order.Chain Mathlib.Order.Closure Mathlib.Order.Cofinal Mathlib.Order.CompleteBooleanAlgebra Mathlib.Order.CompleteLattice.Basic Mathlib.Order.CompleteLattice.Chain Mathlib.Order.CompleteLattice.Defs Mathlib.Order.CompleteLattice.Lemmas Mathlib.Order.Concept Mathlib.Order.ConditionallyCompleteLattice.Basic Mathlib.Order.ConditionallyCompleteLattice.Defs Mathlib.Order.ConditionallyCompleteLattice.Indexed Mathlib.Order.Copy Mathlib.Order.Directed Mathlib.Order.Extension.Linear Mathlib.Order.GaloisConnection.Basic Mathlib.Order.Heyting.Regular Mathlib.Order.Hom.CompleteLattice Mathlib.Order.Hom.Order Mathlib.Order.Hom.Set Mathlib.Order.Interval.Basic Mathlib.Order.Interval.Set.Disjoint Mathlib.Order.Interval.Set.Image Mathlib.Order.Interval.Set.OrderIso Mathlib.Order.Interval.Set.SurjOn Mathlib.Order.Interval.Set.WithBotTop Mathlib.Order.LatticeIntervals Mathlib.Order.Minimal Mathlib.Order.Monotone.Extension Mathlib.Order.Monotone.Union Mathlib.Order.Nucleus Mathlib.Order.OrdContinuous Mathlib.Order.Preorder.Chain Mathlib.Order.Rel.GaloisConnection Mathlib.Order.RelIso.Set Mathlib.Order.ScottContinuity Mathlib.Order.Set Mathlib.Order.WellFounded Mathlib.Order.Zorn Mathlib.SetTheory.Cardinal.Defs Mathlib.SetTheory.ZFC.PSet |
-15 |
120 filesMathlib.Algebra.Order.Nonneg.Lattice Mathlib.Combinatorics.SetFamily.Intersecting Mathlib.Control.EquivFunctor.Instances Mathlib.Control.Functor.Multivariate Mathlib.Data.Fin.Basic Mathlib.Data.Fin.Fin2 Mathlib.Data.Fin.FlagRange Mathlib.Data.Fin.Rev Mathlib.Data.Fin.SuccPred Mathlib.Data.Fin.Tuple.Basic Mathlib.Data.Fin.Tuple.Curry Mathlib.Data.Fin.Tuple.Take Mathlib.Data.Fin.VecNotation Mathlib.Data.Finite.Set Mathlib.Data.Finset.Attach Mathlib.Data.Finset.Basic Mathlib.Data.Finset.BooleanAlgebra Mathlib.Data.Finset.Card Mathlib.Data.Finset.Dedup Mathlib.Data.Finset.Defs Mathlib.Data.Finset.Disjoint Mathlib.Data.Finset.Empty Mathlib.Data.Finset.Erase Mathlib.Data.Finset.Filter Mathlib.Data.Finset.Fin Mathlib.Data.Finset.Fold Mathlib.Data.Finset.Image Mathlib.Data.Finset.Insert Mathlib.Data.Finset.Lattice.Basic Mathlib.Data.Finset.Lattice.Lemmas Mathlib.Data.Finset.Order Mathlib.Data.Finset.Piecewise Mathlib.Data.Finset.Range Mathlib.Data.Finset.SDiff Mathlib.Data.Finset.SymmDiff Mathlib.Data.Fintype.Basic Mathlib.Data.Fintype.Card Mathlib.Data.Fintype.Defs Mathlib.Data.Fintype.EquivFin Mathlib.Data.Fintype.Inv Mathlib.Data.Fintype.OfMap Mathlib.Data.Fintype.Sets Mathlib.Data.Fintype.Shrink Mathlib.Data.List.ChainOfFn Mathlib.Data.List.FinRange Mathlib.Data.List.Lemmas Mathlib.Data.List.NodupEquivFin Mathlib.Data.List.OfFn Mathlib.Data.List.Permutation Mathlib.Data.List.Sort Mathlib.Data.List.Sublists Mathlib.Data.MLList.BestFirst Mathlib.Data.Multiset.Dedup Mathlib.Data.Multiset.Filter Mathlib.Data.Multiset.FinsetOps Mathlib.Data.Multiset.Fold Mathlib.Data.Multiset.Lattice Mathlib.Data.Multiset.MapFold Mathlib.Data.Multiset.NatAntidiagonal Mathlib.Data.Multiset.Range Mathlib.Data.Multiset.Sort Mathlib.Data.Multiset.UnionInter Mathlib.Data.Prod.TProd Mathlib.Data.Set.Constructions Mathlib.Data.Set.Finite.Basic Mathlib.Data.Set.Finite.Range Mathlib.Data.Set.Pairwise.List Mathlib.Data.TypeVec Mathlib.Data.Vector3 Mathlib.Logic.Equiv.Fin.Basic Mathlib.Logic.Equiv.Fintype Mathlib.Logic.Function.FromTypes Mathlib.Logic.Function.OfArity Mathlib.Order.Atoms Mathlib.Order.CompleteLatticeIntervals Mathlib.Order.Cover Mathlib.Order.DirectedInverseSystem Mathlib.Order.Fin.Basic Mathlib.Order.Fin.Finset Mathlib.Order.Fin.SuccAboveOrderIso Mathlib.Order.Fin.Tuple Mathlib.Order.InitialSeg Mathlib.Order.Interval.Set.Fin Mathlib.Order.Interval.Set.Infinite Mathlib.Order.Interval.Set.InitialSeg Mathlib.Order.Interval.Set.Limit Mathlib.Order.Interval.Set.Monotone Mathlib.Order.Interval.Set.OrdConnectedComponent Mathlib.Order.Interval.Set.OrdConnected Mathlib.Order.Interval.Set.OrderEmbedding Mathlib.Order.Interval.Set.ProjIcc Mathlib.Order.Interval.Set.SuccOrder Mathlib.Order.Interval.Set.SuccPred Mathlib.Order.Interval.Set.Union Mathlib.Order.Interval.Set.UnorderedInterval Mathlib.Order.IsNormal Mathlib.Order.ModularLattice Mathlib.Order.PiLex Mathlib.Order.Radical Mathlib.Order.Shrink Mathlib.Order.SuccPred.Archimedean Mathlib.Order.SuccPred.Basic Mathlib.Order.SuccPred.CompleteLinearOrder Mathlib.Order.SuccPred.InitialSeg Mathlib.Order.SuccPred.IntervalSucc Mathlib.Order.SuccPred.Limit Mathlib.Order.SuccPred.Relation Mathlib.Order.SuccPred.Tree Mathlib.Order.SuccPred.WithBot Mathlib.Order.TransfiniteIteration Mathlib.Order.UpperLower.Basic Mathlib.Order.UpperLower.Closure Mathlib.Order.UpperLower.CompleteLattice Mathlib.Order.UpperLower.Fibration Mathlib.Order.UpperLower.Hom Mathlib.Order.UpperLower.Principal Mathlib.Order.UpperLower.Prod Mathlib.Order.ZornAtoms Mathlib.SetTheory.ZFC.Basic Mathlib.Tactic.FinCases |
-14 |
12 filesMathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations Mathlib.AlgebraicTopology.SimplexCategory.Defs Mathlib.CategoryTheory.FinCategory.AsType Mathlib.CategoryTheory.FinCategory.Basic Mathlib.CategoryTheory.MorphismProperty.Basic Mathlib.CategoryTheory.MorphismProperty.Composition Mathlib.CategoryTheory.MorphismProperty.Factorization Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy Mathlib.CategoryTheory.MorphismProperty.IsSmall Mathlib.CategoryTheory.MorphismProperty.Retract Mathlib.CategoryTheory.PathCategory.MorphismProperty Mathlib.CategoryTheory.Widesubcategory |
-13 |
Mathlib.Algebra.GCDMonoid.Nat |
-10 |
Mathlib.Data.Int.GCD |
-5 |
Mathlib.Tactic.NormNum.GCD |
-2 |
212 filesMathlib.Algebra.Algebra.Spectrum.Basic Mathlib.Algebra.Algebra.Spectrum.Pi Mathlib.Algebra.Algebra.Spectrum.Quasispectrum Mathlib.Algebra.Algebra.Subalgebra.Operations Mathlib.Algebra.CharP.Invertible Mathlib.Algebra.Group.WithOne.Basic Mathlib.Algebra.Group.WithOne.Defs Mathlib.Algebra.MvPolynomial.SchwartzZippel Mathlib.Algebra.Notation.Lemmas Mathlib.Algebra.Polynomial.Laurent Mathlib.Algebra.Polynomial.PartialFractions Mathlib.Algebra.Polynomial.Roots Mathlib.Algebra.Star.Unitary Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant Mathlib.CategoryTheory.Adjunction.Comma Mathlib.CategoryTheory.Adjunction.Evaluation Mathlib.CategoryTheory.Adjunction.FullyFaithful Mathlib.CategoryTheory.Adjunction.Limits Mathlib.CategoryTheory.Adjunction.PartialAdjoint Mathlib.CategoryTheory.Adjunction.Reflective Mathlib.CategoryTheory.Adjunction.Triple Mathlib.CategoryTheory.Bicategory.Kan.Adjunction Mathlib.CategoryTheory.Bicategory.Kan.HasKan Mathlib.CategoryTheory.Bicategory.SingleObj Mathlib.CategoryTheory.Category.Cat.Limit Mathlib.CategoryTheory.Category.Factorisation Mathlib.CategoryTheory.Category.Pairwise Mathlib.CategoryTheory.Category.Quiv Mathlib.CategoryTheory.Category.ReflQuiv Mathlib.CategoryTheory.Category.RelCat Mathlib.CategoryTheory.Closed.Monoidal Mathlib.CategoryTheory.Comma.LocallySmall Mathlib.CategoryTheory.Comma.Over.Pullback Mathlib.CategoryTheory.Comma.StructuredArrow.Small Mathlib.CategoryTheory.Countable Mathlib.CategoryTheory.EffectiveEpi.Basic Mathlib.CategoryTheory.EffectiveEpi.Comp Mathlib.CategoryTheory.EffectiveEpi.Coproduct Mathlib.CategoryTheory.EffectiveEpi.Enough Mathlib.CategoryTheory.EffectiveEpi.Preserves Mathlib.CategoryTheory.EffectiveEpi.RegularEpi Mathlib.CategoryTheory.EssentiallySmall Mathlib.CategoryTheory.Functor.Derived.RightDerived Mathlib.CategoryTheory.Functor.KanExtension.Adjunction Mathlib.CategoryTheory.Functor.KanExtension.Basic Mathlib.CategoryTheory.Functor.KanExtension.Pointwise Mathlib.CategoryTheory.Limits.Bicones Mathlib.CategoryTheory.Limits.ColimitLimit Mathlib.CategoryTheory.Limits.ConeCategory Mathlib.CategoryTheory.Limits.Connected Mathlib.CategoryTheory.Limits.Constructions.Over.Connected Mathlib.CategoryTheory.Limits.Constructions.Pullbacks Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial Mathlib.CategoryTheory.Limits.Creates Mathlib.CategoryTheory.Limits.Elements Mathlib.CategoryTheory.Limits.EssentiallySmall Mathlib.CategoryTheory.Limits.Fubini Mathlib.CategoryTheory.Limits.FullSubcategory Mathlib.CategoryTheory.Limits.FunctorCategory.Basic Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks Mathlib.CategoryTheory.Limits.FunctorToTypes Mathlib.CategoryTheory.Limits.HasLimits Mathlib.CategoryTheory.Limits.Pi Mathlib.CategoryTheory.Limits.Preorder Mathlib.CategoryTheory.Limits.Preserves.Basic Mathlib.CategoryTheory.Limits.Preserves.Grothendieck Mathlib.CategoryTheory.Limits.Preserves.Limits Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal Mathlib.CategoryTheory.Limits.Preserves.Ulift Mathlib.CategoryTheory.Limits.Preserves.Yoneda Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts Mathlib.CategoryTheory.Limits.Shapes.Connected Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct Mathlib.CategoryTheory.Limits.Shapes.End Mathlib.CategoryTheory.Limits.Shapes.Equalizers Mathlib.CategoryTheory.Limits.Shapes.Equivalence Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes Mathlib.CategoryTheory.Limits.Shapes.Grothendieck Mathlib.CategoryTheory.Limits.Shapes.Images Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer Mathlib.CategoryTheory.Limits.Shapes.PiProd Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic Mathlib.CategoryTheory.Limits.Shapes.Preorder.Fin Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg Mathlib.CategoryTheory.Limits.Shapes.Products Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone Mathlib.CategoryTheory.Limits.Shapes.RegularMono Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer Mathlib.CategoryTheory.Limits.Shapes.StrictInitial Mathlib.CategoryTheory.Limits.Shapes.Terminal Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects Mathlib.CategoryTheory.Limits.Types.Colimits Mathlib.CategoryTheory.Limits.Types.Images Mathlib.CategoryTheory.Limits.Types.Limits Mathlib.CategoryTheory.Limits.Types.Shapes Mathlib.CategoryTheory.Limits.Types.Yoneda Mathlib.CategoryTheory.Limits.Unit Mathlib.CategoryTheory.Limits.Yoneda Mathlib.CategoryTheory.Localization.Adjunction Mathlib.CategoryTheory.Localization.Bifunctor Mathlib.CategoryTheory.Localization.Bousfield Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions Mathlib.CategoryTheory.Localization.CalculusOfFractions Mathlib.CategoryTheory.Localization.Composition Mathlib.CategoryTheory.Localization.Construction Mathlib.CategoryTheory.Localization.Equivalence Mathlib.CategoryTheory.Localization.HasLocalization Mathlib.CategoryTheory.Localization.HomEquiv Mathlib.CategoryTheory.Localization.LocalizerMorphism Mathlib.CategoryTheory.Localization.LocallySmall Mathlib.CategoryTheory.Localization.Monoidal Mathlib.CategoryTheory.Localization.Opposite Mathlib.CategoryTheory.Localization.Predicate Mathlib.CategoryTheory.Localization.Prod Mathlib.CategoryTheory.Localization.Resolution Mathlib.CategoryTheory.Localization.SmallHom Mathlib.CategoryTheory.Localization.StructuredArrow Mathlib.CategoryTheory.Localization.Trifunctor Mathlib.CategoryTheory.Monad.Adjunction Mathlib.CategoryTheory.Monad.Limits Mathlib.CategoryTheory.Monad.Products Mathlib.CategoryTheory.Monoidal.End Mathlib.CategoryTheory.Monoidal.Free.Basic Mathlib.CategoryTheory.Monoidal.Free.Coherence Mathlib.CategoryTheory.Monoidal.Functor Mathlib.CategoryTheory.Monoidal.NaturalTransformation Mathlib.CategoryTheory.Monoidal.OfChosenFiniteProducts.Basic Mathlib.CategoryTheory.Monoidal.Rigid.Basic Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence Mathlib.CategoryTheory.Monoidal.Transport Mathlib.CategoryTheory.MorphismProperty.Comma Mathlib.CategoryTheory.MorphismProperty.Concrete Mathlib.CategoryTheory.Sites.Closed Mathlib.CategoryTheory.Sites.EffectiveEpimorphic Mathlib.CategoryTheory.Sites.EqualizerSheafCondition Mathlib.CategoryTheory.Sites.Grothendieck Mathlib.CategoryTheory.Sites.IsSheafFor Mathlib.CategoryTheory.Sites.Pretopology Mathlib.CategoryTheory.Sites.SheafOfTypes Mathlib.CategoryTheory.Sites.Sieves Mathlib.CategoryTheory.SmallObject.WellOrderInductionData Mathlib.CategoryTheory.Subpresheaf.Basic Mathlib.CategoryTheory.Subpresheaf.Sieves Mathlib.CategoryTheory.WithTerminal.Basic Mathlib.Combinatorics.Nullstellensatz Mathlib.Combinatorics.Quiver.ReflQuiver Mathlib.Data.Nat.Factorial.NatCast Mathlib.Dynamics.PeriodicPts.Lemmas Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.Order.Category.BddDistLat Mathlib.Order.Category.BddLat Mathlib.Order.Category.BddOrd Mathlib.Order.Category.BoolAlg Mathlib.Order.Category.CompleteLat Mathlib.Order.Category.DistLat Mathlib.Order.Category.Frm Mathlib.Order.Category.HeytAlg Mathlib.Order.Category.Lat Mathlib.Order.Category.LinOrd Mathlib.Order.Category.PartOrd Mathlib.Order.Category.Preord Mathlib.Order.Category.Semilat Mathlib.RingTheory.Algebraic.Cardinality Mathlib.RingTheory.Coprime.Ideal Mathlib.RingTheory.Coprime.Lemmas Mathlib.RingTheory.DividedPowers.Basic Mathlib.RingTheory.DividedPowers.DPMorphism Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal Mathlib.RingTheory.GradedAlgebra.Radical Mathlib.RingTheory.HahnSeries.Valuation Mathlib.RingTheory.Ideal.Colon Mathlib.RingTheory.Ideal.Maps Mathlib.RingTheory.Ideal.Operations Mathlib.RingTheory.Ideal.Pointwise Mathlib.RingTheory.Ideal.Prod Mathlib.RingTheory.Localization.Away.Basic Mathlib.RingTheory.MvPolynomial.EulerIdentity Mathlib.RingTheory.MvPolynomial.Groebner Mathlib.RingTheory.MvPolynomial.Homogeneous Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex Mathlib.RingTheory.MvPolynomial.MonomialOrder Mathlib.RingTheory.Polynomial.HilbertPoly Mathlib.RingTheory.Polynomial.Ideal Mathlib.RingTheory.PowerSeries.NoZeroDivisors Mathlib.RingTheory.UniqueFactorizationDomain.Ideal Mathlib.RingTheory.Valuation.Basic Mathlib.RingTheory.Valuation.Discrete.Basic Mathlib.RingTheory.Valuation.ExtendToLocalization Mathlib.RingTheory.Valuation.Integers Mathlib.RingTheory.Valuation.PrimeMultiplicity Mathlib.RingTheory.Valuation.RankOne Mathlib.RingTheory.Valuation.ValExtension Mathlib.Tactic.CategoryTheory.Coherence Mathlib.Tactic.NormNum.IsCoprime Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology |
-1 |
Mathlib.Control.Traversable.Basic Mathlib.Data.Option.Defs |
1 |
Declarations diff
+ CommRing.toGrindCommRing
+ CommRing.toGrindCommRing_ofNat
+ _root_.Lean.SearchPath.relativize
+ instance (X : Type u) [TopologicalSpace X] [Small.{v} X] :
+ instance (α : Type*) [CommRing α] (n : ℕ) [CharP α n] : Lean.Grind.IsCharP α n
+ instance [NormedField 𝕜] [NormedCommRing R] [NormedAlgebra 𝕜 R] :
+ merge_isAssociative
+ merge_isCommutative
+ merge_isId
+ merge_isIdempotent
++-- toAffine
+-+--+ of_surjective
- One
- decidableEqNone
- decidableExistsMem
- decidableForallMem
- div_dvd_iff_dvd_mul
- div_eq_self
- div_pow
- drop_sum_flatten'
- drop_sum_join'
- drop_take_succ_flatten_eq_getElem'
- drop_take_succ_join_eq_getElem'
- dvd_gcd
- eq_none_iff_forall_some_ne
- eq_none_or_eq_some
- exists_ne_none
- gcd_assoc
- gcd_comm
- gcd_dvd_gcd_mul_left_right
- gcd_dvd_gcd_mul_right_right
- gcd_dvd_gcd_of_dvd_left
- gcd_dvd_gcd_of_dvd_right
- gcd_eq_left
- gcd_eq_right
- gcd_eq_zero_iff
- gcd_mul_lcm
- gcd_mul_left
- gcd_mul_right
- gcd_natCast_natCast
- gcd_pos_iff
- gcd_pos_of_ne_zero_left
- gcd_pos_of_ne_zero_right
- gcd_self
- gcd_zero_left
- gcd_zero_right
- instance (X : Type u) [TopologicalSpace X] [Small.{v} X] : TopologicalSpace (Shrink.{v} X)
- instance (priority := 200) One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α
- instance (priority := 300) One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1)
- instance : Pow (BitVec w) ℕ := ⟨fun x n => ofFin <| x.toFin ^ n⟩
- instance [NormedField 𝕜] [NormedCommRing R] [NormedAlgebra 𝕜 R] : NormedSpace 𝕜 C(α, R)₀
- isNone_eq_false_iff
- lcm_assoc
- lcm_comm
- lcm_dvd
- lcm_dvd_iff
- lcm_dvd_mul
- lcm_one_left
- lcm_one_right
- lcm_pos
- lcm_zero_left
- lcm_zero_right
- mem_some_iff
- mul_dvd_mul
- mul_dvd_mul_iff_left
- mul_dvd_mul_iff_right
- natAbs_ediv_of_dvd
- natAbs_pow
- pbind_eq_bind
- pbind_eq_some
- pbind_map
- pow_dvd_pow_iff
- take_sum_flatten'
- take_sum_join'
-+-+ iic
-+-+-+-+ colimitCoconeIsColimit
-- lcm_mul_left
-- lcm_mul_right
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) = (0.89, 0.02)
| Current number | Change | Type |
|---|---|---|
| 130 | 8 | adaptation notes |
| 71 | -3 | disabled deprecation lints |
Current commit b460494b92
Reference commit 0d9eafd4f7
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).
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
6 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.
No description provided.