[Merged by Bors] - chore(Algebra/Group/Hom/Instances): tidy and cancellativity#27318
Closed
eric-wieser wants to merge 6 commits intomasterfrom
Closed
[Merged by Bors] - chore(Algebra/Group/Hom/Instances): tidy and cancellativity#27318eric-wieser wants to merge 6 commits intomasterfrom
eric-wieser wants to merge 6 commits intomasterfrom
Conversation
PR summary f1a92a38b2Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Algebra.Group.Hom.Instances | 129 | 143 | +14 (+10.85%) |
Import changes for all files
| Files | Import difference |
|---|---|
644 filesMathlib.Algebra.Algebra.Defs Mathlib.Algebra.Algebra.Rat Mathlib.Algebra.BigOperators.Fin Mathlib.Algebra.BigOperators.Finprod Mathlib.Algebra.BigOperators.Group.Finset.Indicator Mathlib.Algebra.BigOperators.Group.Finset.Lemmas Mathlib.Algebra.BigOperators.GroupWithZero.Action Mathlib.Algebra.BigOperators.Module Mathlib.Algebra.BigOperators.Pi Mathlib.Algebra.BigOperators.Ring.Finset Mathlib.Algebra.BigOperators.Ring.Multiset Mathlib.Algebra.BigOperators.Ring.Nat Mathlib.Algebra.BigOperators.RingEquiv Mathlib.Algebra.BigOperators.WithTop Mathlib.Algebra.Category.Grp.Basic Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup Mathlib.Algebra.Category.Grp.FilteredColimits Mathlib.Algebra.Category.Grp.FiniteGrp Mathlib.Algebra.Category.Grp.ForgetCorepresentable Mathlib.Algebra.Category.Grp.Preadditive Mathlib.Algebra.Category.Grp.Yoneda Mathlib.Algebra.Category.Grp.ZModuleEquivalence Mathlib.Algebra.Category.Grp.Zero Mathlib.Algebra.Category.ModuleCat.Basic Mathlib.Algebra.Category.MonCat.Yoneda Mathlib.Algebra.Category.Ring.Basic Mathlib.Algebra.Category.Ring.Colimits Mathlib.Algebra.Category.Ring.FilteredColimits Mathlib.Algebra.CharP.Basic Mathlib.Algebra.CharP.Defs Mathlib.Algebra.CharP.Invertible Mathlib.Algebra.CharP.Pi Mathlib.Algebra.Colimit.DirectLimit Mathlib.Algebra.ContinuedFractions.Computation.Basic Mathlib.Algebra.Field.Opposite Mathlib.Algebra.Field.Power Mathlib.Algebra.Field.Rat Mathlib.Algebra.GCDMonoid.Basic Mathlib.Algebra.GCDMonoid.Finset Mathlib.Algebra.GCDMonoid.Multiset Mathlib.Algebra.GCDMonoid.Nat Mathlib.Algebra.GCDMonoid.PUnit Mathlib.Algebra.GeomSum Mathlib.Algebra.Group.ConjFinite Mathlib.Algebra.Group.EvenFunction Mathlib.Algebra.Group.NatPowAssoc Mathlib.Algebra.Group.Pointwise.Finset.Interval Mathlib.Algebra.Group.Pointwise.Set.Card Mathlib.Algebra.Group.Translate Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card Mathlib.Algebra.Homology.Additive Mathlib.Algebra.Homology.Augment Mathlib.Algebra.Homology.CommSq Mathlib.Algebra.Homology.DifferentialObject Mathlib.Algebra.Homology.Double Mathlib.Algebra.Homology.Embedding.Boundary Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.ExactSequence Mathlib.Algebra.Homology.Factorizations.Basic Mathlib.Algebra.Homology.Functor Mathlib.Algebra.Homology.GrothendieckAbelian Mathlib.Algebra.Homology.HomologicalBicomplex Mathlib.Algebra.Homology.HomologicalComplexAbelian Mathlib.Algebra.Homology.HomologicalComplexBiprod Mathlib.Algebra.Homology.HomologicalComplexLimits Mathlib.Algebra.Homology.HomologicalComplex Mathlib.Algebra.Homology.ImageToKernel Mathlib.Algebra.Homology.Linear Mathlib.Algebra.Homology.ShortComplex.Abelian Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.Algebra.Homology.ShortComplex.Exact Mathlib.Algebra.Homology.ShortComplex.Linear Mathlib.Algebra.Homology.ShortComplex.Preadditive Mathlib.Algebra.Homology.ShortComplex.ShortExact Mathlib.Algebra.Homology.ShortComplex.SnakeLemma Mathlib.Algebra.Homology.Single Mathlib.Algebra.Homology.Square Mathlib.Algebra.IsPrimePow Mathlib.Algebra.Module.Basic Mathlib.Algebra.Module.BigOperators Mathlib.Algebra.Module.Card Mathlib.Algebra.Module.End Mathlib.Algebra.Module.Equiv.Basic Mathlib.Algebra.Module.Equiv.Defs Mathlib.Algebra.Module.Equiv.Opposite Mathlib.Algebra.Module.Hom Mathlib.Algebra.Module.LinearMap.Basic Mathlib.Algebra.Module.LinearMap.Defs Mathlib.Algebra.Module.LinearMap.End Mathlib.Algebra.Module.LinearMap.Prod Mathlib.Algebra.Module.LinearMap.Rat Mathlib.Algebra.Module.LinearMap.Star Mathlib.Algebra.Module.NatInt Mathlib.Algebra.Module.Opposite Mathlib.Algebra.Module.PUnit Mathlib.Algebra.Module.Pi Mathlib.Algebra.Module.Rat Mathlib.Algebra.Module.RingHom Mathlib.Algebra.Module.Shrink Mathlib.Algebra.Module.TransferInstance Mathlib.Algebra.Module.ULift Mathlib.Algebra.NoZeroSMulDivisors.Basic Mathlib.Algebra.Order.AbsoluteValue.Basic Mathlib.Algebra.Order.AbsoluteValue.Euclidean Mathlib.Algebra.Order.Algebra Mathlib.Algebra.Order.Antidiag.Pi Mathlib.Algebra.Order.BigOperators.Ring.List Mathlib.Algebra.Order.BigOperators.Ring.Multiset Mathlib.Algebra.Order.CauSeq.Basic Mathlib.Algebra.Order.Field.Basic Mathlib.Algebra.Order.Field.Canonical Mathlib.Algebra.Order.Field.Power Mathlib.Algebra.Order.Floor.Defs Mathlib.Algebra.Order.Group.Indicator Mathlib.Algebra.Order.Group.Int.Sum Mathlib.Algebra.Order.Group.Pointwise.Interval Mathlib.Algebra.Order.Hom.Ring Mathlib.Algebra.Order.Interval.Basic Mathlib.Algebra.Order.Invertible Mathlib.Algebra.Order.Kleene Mathlib.Algebra.Order.Module.Algebra Mathlib.Algebra.Order.Module.Basic Mathlib.Algebra.Order.Module.Defs Mathlib.Algebra.Order.Module.Field Mathlib.Algebra.Order.Module.OrderedSMul Mathlib.Algebra.Order.Module.Pointwise Mathlib.Algebra.Order.Module.PositiveLinearMap Mathlib.Algebra.Order.Monovary Mathlib.Algebra.Order.Nonneg.Basic Mathlib.Algebra.Order.Nonneg.Floor Mathlib.Algebra.Order.Pi Mathlib.Algebra.Order.Rearrangement Mathlib.Algebra.Order.Ring.Abs Mathlib.Algebra.Order.Ring.Basic Mathlib.Algebra.Order.Ring.Canonical Mathlib.Algebra.Order.Ring.Cast Mathlib.Algebra.Order.Ring.Cone Mathlib.Algebra.Order.Ring.Finset Mathlib.Algebra.Order.Ring.Int Mathlib.Algebra.Order.Ring.Nat Mathlib.Algebra.Order.Ring.Pow Mathlib.Algebra.Order.Ring.Prod Mathlib.Algebra.Order.Ring.Rat Mathlib.Algebra.Order.Ring.Unbundled.Rat Mathlib.Algebra.Order.Ring.WithTop Mathlib.Algebra.Order.WithTop.Untop0 Mathlib.Algebra.Regular.Pi Mathlib.Algebra.Regular.Prod Mathlib.Algebra.Regular.SMul Mathlib.Algebra.Regular.ULift Mathlib.Algebra.Ring.Action.Basic Mathlib.Algebra.Ring.Action.End Mathlib.Algebra.Ring.Action.Field Mathlib.Algebra.Ring.Action.Group Mathlib.Algebra.Ring.AddAut Mathlib.Algebra.Ring.Associated Mathlib.Algebra.Ring.Associator Mathlib.Algebra.Ring.Aut Mathlib.Algebra.Ring.Center Mathlib.Algebra.Ring.CharZero Mathlib.Algebra.Ring.Int.Parity Mathlib.Algebra.Ring.Parity Mathlib.Algebra.Ring.Pi Mathlib.Algebra.Ring.Prod Mathlib.Algebra.Ring.Subsemiring.Order Mathlib.Algebra.Star.Basic Mathlib.Algebra.Star.BigOperators Mathlib.Algebra.Star.Center Mathlib.Algebra.Star.Conjneg Mathlib.Algebra.Star.Pi Mathlib.Algebra.Star.Pointwise Mathlib.Algebra.Star.Prod Mathlib.Algebra.Star.Rat Mathlib.Algebra.Star.StarRingHom Mathlib.CategoryTheory.Abelian.Basic Mathlib.CategoryTheory.Abelian.CommSq Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel Mathlib.CategoryTheory.Abelian.Exact Mathlib.CategoryTheory.Abelian.FunctorCategory Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject Mathlib.CategoryTheory.Abelian.Monomorphisms Mathlib.CategoryTheory.Abelian.NonPreadditive Mathlib.CategoryTheory.Abelian.Opposite Mathlib.CategoryTheory.Abelian.Refinements Mathlib.CategoryTheory.Abelian.SerreClass.Basic Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty Mathlib.CategoryTheory.Abelian.Subobject Mathlib.CategoryTheory.Abelian.Transfer Mathlib.CategoryTheory.Action.Basic Mathlib.CategoryTheory.Action.Limits Mathlib.CategoryTheory.Adjunction.Additive Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems Mathlib.CategoryTheory.Center.Linear Mathlib.CategoryTheory.Center.Localization Mathlib.CategoryTheory.Comma.CardinalArrow Mathlib.CategoryTheory.Dialectica.Monoidal Mathlib.CategoryTheory.Distributive.Cartesian Mathlib.CategoryTheory.Distributive.Monoidal Mathlib.CategoryTheory.Galois.Basic Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Generator.HomologicalComplex Mathlib.CategoryTheory.Generator.Preadditive Mathlib.CategoryTheory.Generator.Presheaf Mathlib.CategoryTheory.Generator.Sheaf Mathlib.CategoryTheory.Idempotents.Basic Mathlib.CategoryTheory.Idempotents.Biproducts Mathlib.CategoryTheory.Idempotents.FunctorCategories Mathlib.CategoryTheory.Idempotents.FunctorExtension Mathlib.CategoryTheory.Idempotents.HomologicalComplex Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi Mathlib.CategoryTheory.Idempotents.Karoubi Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures Mathlib.CategoryTheory.Limits.SmallComplete Mathlib.CategoryTheory.Linear.Basic Mathlib.CategoryTheory.Linear.FunctorCategory Mathlib.CategoryTheory.Linear.LinearFunctor Mathlib.CategoryTheory.Linear.Yoneda Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive Mathlib.CategoryTheory.Localization.Linear Mathlib.CategoryTheory.Localization.Preadditive Mathlib.CategoryTheory.Localization.SmallShiftedHom Mathlib.CategoryTheory.Monoidal.Linear Mathlib.CategoryTheory.Monoidal.Preadditive Mathlib.CategoryTheory.Monoidal.Subcategory Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.ObjectProperty.EpiMono Mathlib.CategoryTheory.ObjectProperty.Extensions Mathlib.CategoryTheory.Preadditive.AdditiveFunctor Mathlib.CategoryTheory.Preadditive.Basic Mathlib.CategoryTheory.Preadditive.Biproducts Mathlib.CategoryTheory.Preadditive.EilenbergMoore Mathlib.CategoryTheory.Preadditive.EndoFunctor Mathlib.CategoryTheory.Preadditive.FunctorCategory Mathlib.CategoryTheory.Preadditive.LeftExact Mathlib.CategoryTheory.Preadditive.LiftToFinset Mathlib.CategoryTheory.Preadditive.Mat Mathlib.CategoryTheory.Preadditive.Opposite Mathlib.CategoryTheory.Preadditive.SingleObj Mathlib.CategoryTheory.Preadditive.Transfer Mathlib.CategoryTheory.Preadditive.Yoneda.Basic Mathlib.CategoryTheory.Presentable.Basic Mathlib.CategoryTheory.Presentable.Finite Mathlib.CategoryTheory.Presentable.IsCardinalFiltered Mathlib.CategoryTheory.Presentable.Limits Mathlib.CategoryTheory.Quotient.Linear Mathlib.CategoryTheory.Quotient.Preadditive Mathlib.CategoryTheory.Shift.InducedShiftSequence Mathlib.CategoryTheory.Shift.Linear Mathlib.CategoryTheory.Shift.Opposite Mathlib.CategoryTheory.Shift.Pullback Mathlib.CategoryTheory.Shift.ShiftSequence Mathlib.CategoryTheory.Shift.ShiftedHomOpposite Mathlib.CategoryTheory.Shift.ShiftedHom Mathlib.CategoryTheory.Simple Mathlib.CategoryTheory.Sites.Abelian Mathlib.CategoryTheory.Sites.Adjunction Mathlib.CategoryTheory.Sites.Canonical Mathlib.CategoryTheory.Sites.CartesianClosed Mathlib.CategoryTheory.Sites.CartesianMonoidal Mathlib.CategoryTheory.Sites.ChosenFiniteProducts Mathlib.CategoryTheory.Sites.Coherent.Basic Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology Mathlib.CategoryTheory.Sites.Coherent.Comparison Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves Mathlib.CategoryTheory.Sites.Coherent.RegularTopology Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.CategoryTheory.Sites.CompatiblePlus Mathlib.CategoryTheory.Sites.CompatibleSheafification Mathlib.CategoryTheory.Sites.ConcreteSheafification Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.CategoryTheory.Sites.Continuous Mathlib.CategoryTheory.Sites.CoverLifting Mathlib.CategoryTheory.Sites.CoverPreserving Mathlib.CategoryTheory.Sites.Coverage Mathlib.CategoryTheory.Sites.CoversTop Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.CategoryTheory.Sites.EpiMono Mathlib.CategoryTheory.Sites.Equivalence Mathlib.CategoryTheory.Sites.GlobalSections Mathlib.CategoryTheory.Sites.IsSheafOneHypercover Mathlib.CategoryTheory.Sites.LeftExact Mathlib.CategoryTheory.Sites.Limits Mathlib.CategoryTheory.Sites.Localization Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 Mathlib.CategoryTheory.Sites.OneHypercover Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.Plus Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.PreservesSheafification Mathlib.CategoryTheory.Sites.Pullback Mathlib.CategoryTheory.Sites.SheafHom Mathlib.CategoryTheory.Sites.Sheaf Mathlib.CategoryTheory.Sites.Sheafification Mathlib.CategoryTheory.Sites.Subcanonical Mathlib.CategoryTheory.Sites.Subsheaf Mathlib.CategoryTheory.Sites.Types Mathlib.CategoryTheory.Sites.Whiskering Mathlib.CategoryTheory.Sites.ZeroHypercover Mathlib.CategoryTheory.SmallObject.Basic Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument Mathlib.CategoryTheory.Subobject.FactorThru Mathlib.CategoryTheory.Subobject.HasCardinalLT Mathlib.CategoryTheory.Subobject.Lattice Mathlib.CategoryTheory.Subobject.Limits Mathlib.CategoryTheory.Subobject.NoetherianObject Mathlib.CategoryTheory.Triangulated.Opposite.Basic Mathlib.CategoryTheory.Triangulated.Opposite.Triangle Mathlib.CategoryTheory.Triangulated.Rotate Mathlib.Combinatorics.Additive.Dissociation Mathlib.Combinatorics.Colex Mathlib.Combinatorics.Enumerative.Composition Mathlib.Combinatorics.Enumerative.DoubleCounting Mathlib.Combinatorics.Enumerative.IncidenceAlgebra Mathlib.Combinatorics.Enumerative.InclusionExclusion Mathlib.Combinatorics.Enumerative.Partition Mathlib.Combinatorics.Pigeonhole Mathlib.Combinatorics.SetFamily.Compression.UV Mathlib.Combinatorics.SetFamily.HarrisKleitman Mathlib.Combinatorics.SetFamily.Kleitman Mathlib.Combinatorics.SetFamily.KruskalKatona Mathlib.Combinatorics.SetFamily.Shadow Mathlib.Combinatorics.SimpleGraph.Circulant Mathlib.Combinatorics.SimpleGraph.Clique Mathlib.Combinatorics.SimpleGraph.Coloring Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite Mathlib.Combinatorics.SimpleGraph.ConcreteColorings Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting Mathlib.Combinatorics.SimpleGraph.Diam Mathlib.Combinatorics.SimpleGraph.FiveWheelLike Mathlib.Combinatorics.SimpleGraph.Hasse Mathlib.Combinatorics.SimpleGraph.IncMatrix Mathlib.Combinatorics.SimpleGraph.Metric Mathlib.Combinatorics.SimpleGraph.Partition Mathlib.Combinatorics.SimpleGraph.Prod Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise Mathlib.Combinatorics.SimpleGraph.Sum Mathlib.Combinatorics.SimpleGraph.Trails Mathlib.Combinatorics.SimpleGraph.Turan Mathlib.Computability.ContextFreeGrammar Mathlib.Computability.Encoding Mathlib.Computability.Halting Mathlib.Computability.Language Mathlib.Computability.PartrecCode Mathlib.Computability.Partrec Mathlib.Computability.Primrec Mathlib.Computability.Reduce Mathlib.Computability.RegularExpressions Mathlib.Computability.TMConfig Mathlib.Computability.TMToPartrec Mathlib.Computability.TuringDegree Mathlib.Data.BitVec Mathlib.Data.Bool.Count Mathlib.Data.DFinsupp.Lex Mathlib.Data.DFinsupp.Module Mathlib.Data.DFinsupp.Order Mathlib.Data.DFinsupp.Sigma Mathlib.Data.DFinsupp.WellFounded Mathlib.Data.ENat.Basic Mathlib.Data.ENat.BigOperators Mathlib.Data.ENat.Lattice Mathlib.Data.Fin.Parity Mathlib.Data.Fin.Tuple.NatAntidiagonal Mathlib.Data.Fin.Tuple.Reflection Mathlib.Data.Finite.Card Mathlib.Data.Finite.Perm Mathlib.Data.Finset.Grade Mathlib.Data.Finset.Interval Mathlib.Data.Finset.NatDivisors Mathlib.Data.Finset.NoncommProd Mathlib.Data.Fintype.Units Mathlib.Data.Holor Mathlib.Data.Int.AbsoluteValue Mathlib.Data.Int.Associated Mathlib.Data.Int.Cast.Lemmas Mathlib.Data.Int.CharZero Mathlib.Data.Int.Interval Mathlib.Data.Int.Lemmas Mathlib.Data.Int.NatPrime Mathlib.Data.Int.Order.Lemmas Mathlib.Data.Int.Order.Units Mathlib.Data.Int.Range Mathlib.Data.Int.SuccPred Mathlib.Data.Matrix.CharP Mathlib.Data.Matrix.Defs Mathlib.Data.Matrix.Diagonal Mathlib.Data.Matrix.Mul Mathlib.Data.Matrix.PEquiv Mathlib.Data.Matroid.Basic Mathlib.Data.Matroid.Circuit Mathlib.Data.Matroid.Closure Mathlib.Data.Matroid.Constructions Mathlib.Data.Matroid.Dual Mathlib.Data.Matroid.IndepAxioms Mathlib.Data.Matroid.Loop Mathlib.Data.Matroid.Map Mathlib.Data.Matroid.Minor.Contract Mathlib.Data.Matroid.Minor.Delete Mathlib.Data.Matroid.Minor.Order Mathlib.Data.Matroid.Minor.Restrict Mathlib.Data.Matroid.Rank.Cardinal Mathlib.Data.Matroid.Rank.ENat Mathlib.Data.Matroid.Rank.Finite Mathlib.Data.Matroid.Sum Mathlib.Data.NNRat.Defs Mathlib.Data.Nat.BitIndices Mathlib.Data.Nat.Cast.Basic Mathlib.Data.Nat.Cast.Field Mathlib.Data.Nat.Cast.Order.Basic Mathlib.Data.Nat.Cast.Order.Field Mathlib.Data.Nat.Cast.Order.Ring Mathlib.Data.Nat.Cast.SetInterval Mathlib.Data.Nat.ChineseRemainder Mathlib.Data.Nat.Choose.Bounds Mathlib.Data.Nat.Choose.Dvd Mathlib.Data.Nat.Choose.Mul Mathlib.Data.Nat.Dist Mathlib.Data.Nat.EvenOddRec Mathlib.Data.Nat.Factorial.NatCast Mathlib.Data.Nat.Factors Mathlib.Data.Nat.MaxPowDiv Mathlib.Data.Nat.Prime.Basic Mathlib.Data.Nat.Prime.Factorial Mathlib.Data.Nat.Prime.Int Mathlib.Data.Nat.Prime.Pow Mathlib.Data.Nat.PrimeFin Mathlib.Data.Num.Lemmas Mathlib.Data.Num.ZNum Mathlib.Data.Ordmap.Invariants Mathlib.Data.Ordmap.Ordset Mathlib.Data.Rat.BigOperators Mathlib.Data.Rat.Cardinal Mathlib.Data.Rat.Cast.CharZero Mathlib.Data.Rat.Cast.Defs Mathlib.Data.Rat.Lemmas Mathlib.Data.Rat.Sqrt Mathlib.Data.Set.Card.Arithmetic Mathlib.Data.Set.Card Mathlib.Data.Set.Semiring Mathlib.Data.Setoid.Partition.Card Mathlib.Data.Sign Mathlib.Data.W.Cardinal Mathlib.Dynamics.BirkhoffSum.Average Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Geometry.RingedSpace.Stalks Mathlib.GroupTheory.GroupAction.DomAct.ActionHom Mathlib.GroupTheory.GroupAction.DomAct.Basic Mathlib.GroupTheory.GroupAction.Hom Mathlib.GroupTheory.GroupAction.Pointwise Mathlib.GroupTheory.Perm.List Mathlib.GroupTheory.Perm.Support Mathlib.LinearAlgebra.GeneralLinearGroup Mathlib.LinearAlgebra.Matrix.Integer Mathlib.LinearAlgebra.Matrix.Orthogonal Mathlib.Logic.Godel.GodelBetaFunction Mathlib.MeasureTheory.MeasurableSpace.Basic Mathlib.MeasureTheory.MeasurableSpace.Card Mathlib.ModelTheory.Algebra.Field.Basic Mathlib.ModelTheory.Algebra.Ring.Basic Mathlib.ModelTheory.Basic Mathlib.ModelTheory.Bundled Mathlib.ModelTheory.Complexity Mathlib.ModelTheory.Definability Mathlib.ModelTheory.DirectLimit Mathlib.ModelTheory.ElementaryMaps Mathlib.ModelTheory.ElementarySubstructures Mathlib.ModelTheory.Encoding Mathlib.ModelTheory.Equivalence Mathlib.ModelTheory.FinitelyGenerated Mathlib.ModelTheory.Graph Mathlib.ModelTheory.LanguageMap Mathlib.ModelTheory.PartialEquiv Mathlib.ModelTheory.Quotients Mathlib.ModelTheory.Satisfiability Mathlib.ModelTheory.Semantics Mathlib.ModelTheory.Skolem Mathlib.ModelTheory.Substructures Mathlib.ModelTheory.Syntax Mathlib.ModelTheory.Types Mathlib.ModelTheory.Ultraproducts Mathlib.NumberTheory.Divisors Mathlib.NumberTheory.Padics.PadicVal.Defs Mathlib.Order.Extension.Well Mathlib.Order.Filter.AtTopBot.ModEq Mathlib.Order.Filter.EventuallyConst Mathlib.Order.Filter.FilterProduct Mathlib.Order.Filter.Germ.Basic Mathlib.Order.Filter.Germ.OrderedMonoid Mathlib.Order.Filter.IndicatorFunction Mathlib.Order.Filter.Ring Mathlib.Order.Grade Mathlib.Order.Height Mathlib.Order.Interval.Set.IsoIoo Mathlib.Order.Interval.Set.OrdConnectedLinear Mathlib.Order.JordanHolder Mathlib.Order.KonigLemma Mathlib.Order.KrullDimension Mathlib.Order.Monotone.MonovaryOrder Mathlib.Order.Partition.Equipartition Mathlib.Order.RelSeries Mathlib.RingTheory.Congruence.Defs Mathlib.RingTheory.Invariant.Defs Mathlib.RingTheory.Multiplicity Mathlib.RingTheory.Prime Mathlib.SetTheory.Cardinal.Aleph Mathlib.SetTheory.Cardinal.Arithmetic Mathlib.SetTheory.Cardinal.Basic Mathlib.SetTheory.Cardinal.Cofinality Mathlib.SetTheory.Cardinal.Continuum Mathlib.SetTheory.Cardinal.CountableCover Mathlib.SetTheory.Cardinal.Divisibility Mathlib.SetTheory.Cardinal.ENat Mathlib.SetTheory.Cardinal.Embedding Mathlib.SetTheory.Cardinal.Finite Mathlib.SetTheory.Cardinal.HasCardinalLT Mathlib.SetTheory.Cardinal.NatCount Mathlib.SetTheory.Cardinal.Order Mathlib.SetTheory.Cardinal.Ordinal Mathlib.SetTheory.Cardinal.Pigeonhole Mathlib.SetTheory.Cardinal.Regular Mathlib.SetTheory.Cardinal.ToNat Mathlib.SetTheory.Cardinal.UnivLE Mathlib.SetTheory.Game.Basic Mathlib.SetTheory.Game.Birthday Mathlib.SetTheory.Game.Domineering Mathlib.SetTheory.Game.Impartial Mathlib.SetTheory.Game.Nim Mathlib.SetTheory.Game.Ordinal Mathlib.SetTheory.Game.Short Mathlib.SetTheory.Game.State Mathlib.SetTheory.Lists Mathlib.SetTheory.Nimber.Basic Mathlib.SetTheory.Ordinal.Arithmetic Mathlib.SetTheory.Ordinal.Basic Mathlib.SetTheory.Ordinal.CantorNormalForm Mathlib.SetTheory.Ordinal.Enum Mathlib.SetTheory.Ordinal.Exponential Mathlib.SetTheory.Ordinal.Family Mathlib.SetTheory.Ordinal.FixedPointApproximants Mathlib.SetTheory.Ordinal.FixedPoint Mathlib.SetTheory.Ordinal.NaturalOps Mathlib.SetTheory.Ordinal.Principal Mathlib.SetTheory.Ordinal.Rank Mathlib.SetTheory.Ordinal.Veblen Mathlib.SetTheory.Surreal.Basic Mathlib.SetTheory.ZFC.Rank Mathlib.Tactic.Abel Mathlib.Tactic.Bound Mathlib.Tactic.CancelDenoms Mathlib.Tactic.ENatToNat Mathlib.Tactic.FieldSimp Mathlib.Tactic.Finiteness Mathlib.Tactic.Linarith.Datatypes Mathlib.Tactic.Linarith.Frontend Mathlib.Tactic.Linarith.Lemmas Mathlib.Tactic.Linarith.Oracle.FourierMotzkin Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm Mathlib.Tactic.Linarith.Parsing Mathlib.Tactic.Linarith.Preprocessing Mathlib.Tactic.Linarith.Verification Mathlib.Tactic.LinearCombination.Lemmas Mathlib.Tactic.NoncommRing Mathlib.Tactic.NormNum.Basic Mathlib.Tactic.NormNum.BigOperators Mathlib.Tactic.NormNum.DivMod Mathlib.Tactic.NormNum.Eq Mathlib.Tactic.NormNum.Ineq Mathlib.Tactic.NormNum.Inv Mathlib.Tactic.NormNum.PowMod Mathlib.Tactic.NormNum.Pow Mathlib.Tactic.NormNum.Prime Mathlib.Tactic.Positivity.Basic Mathlib.Tactic.Positivity.Core Mathlib.Tactic.Qify Mathlib.Tactic.Ring.Basic Mathlib.Tactic.Ring.Compare Mathlib.Tactic.Ring.RingNF Mathlib.Tactic.Simproc.Divisors Mathlib.Tactic.Simproc.Factors Mathlib.Topology.Algebra.Constructions.DomMulAct Mathlib.Topology.Algebra.Indicator Mathlib.Topology.Algebra.InfiniteSum.Basic Mathlib.Topology.Algebra.InfiniteSum.Defs Mathlib.Topology.Algebra.Order.Support Mathlib.Topology.Algebra.Star Mathlib.Topology.Algebra.Support Mathlib.Topology.Category.CompHausLike.EffectiveEpi Mathlib.Topology.DiscreteQuotient Mathlib.Topology.FiberPartition Mathlib.Topology.IndicatorConstPointwise Mathlib.Topology.KrullDimension Mathlib.Topology.LocallyConstant.Basic Mathlib.Topology.Separation.DisjointCover Mathlib.Topology.Sheaves.Alexandrov Mathlib.Topology.Sheaves.Forget Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Sheaves.Limits Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Topology.Sheaves.PUnit Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Topology.Sheaves.Sheaf Mathlib.Topology.Sheaves.Sheafify Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.Stalks Mathlib.Topology.UniformSpace.AbsoluteValue Mathlib.Topology.UniformSpace.HeineCantor |
1 |
20 filesMathlib.Algebra.BigOperators.Ring.List Mathlib.Algebra.Field.Shrink Mathlib.Algebra.Field.TransferInstance Mathlib.Algebra.Field.ULift Mathlib.Algebra.Group.Indicator Mathlib.Algebra.Group.Pi.Lemmas Mathlib.Algebra.GroupWithZero.Indicator Mathlib.Algebra.Order.Ring.Opposite Mathlib.Algebra.Ring.CompTypeclasses Mathlib.Algebra.Ring.Equiv Mathlib.Algebra.Ring.Fin Mathlib.Algebra.Ring.Opposite Mathlib.Algebra.Ring.Shrink Mathlib.Algebra.Ring.Subring.Defs Mathlib.Algebra.Ring.Subsemiring.Defs Mathlib.Algebra.Ring.TransferInstance Mathlib.Algebra.Ring.ULift Mathlib.RingTheory.NonUnitalSubring.Defs Mathlib.RingTheory.NonUnitalSubsemiring.Defs Mathlib.RingTheory.RingInvo |
2 |
10 filesMathlib.Algebra.EuclideanDomain.Basic Mathlib.Algebra.Field.Basic Mathlib.Algebra.Order.Sub.Unbundled.Hom Mathlib.Algebra.Ring.Commute Mathlib.Algebra.Ring.Hom.Basic Mathlib.Algebra.Ring.Int.Units Mathlib.Algebra.Ring.Units Mathlib.Data.Nat.Cast.Commute Mathlib.Data.Rat.Denumerable Mathlib.Tactic.CancelDenoms.Core |
3 |
4 filesMathlib.Algebra.Ring.Basic Mathlib.Algebra.Ring.Hom.Defs Mathlib.Algebra.Ring.Rat Mathlib.Deprecated.RingHom |
4 |
Mathlib.Algebra.Group.Hom.End |
13 |
Mathlib.Algebra.Group.Hom.Instances |
14 |
Declarations diff
+ AddMonoidHom.instIntSMul
+ AddMonoidHom.instNatSMul
+ MonoidHom.instIntPow
+ MonoidHom.instPow
+ MonoidHom.zpow_apply
+ instance [MulOneClass M] [CommMonoid N] [IsCancelMul N] : IsCancelMul (M →* N)
+ instance [MulOneClass M] [CommMonoid N] [IsLeftCancelMul N] : IsLeftCancelMul (M →* N)
+ instance [MulOneClass M] [CommMonoid N] [IsRightCancelMul N] : IsRightCancelMul (M →* N)
+ isCancelMul
+ isLeftCancelMul
+ isRightCancelMul
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.
No changes to technical debt.
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).
eric-wieser
commented
Jul 20, 2025
YaelDillies
reviewed
Jul 21, 2025
YaelDillies
approved these changes
Jul 22, 2025
Contributor
YaelDillies
left a comment
There was a problem hiding this comment.
Thanks!
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
1 task
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jul 23, 2025
These can be constructed with less work via the injectivity constructors. This also adds the cancellative instances.
Contributor
|
Pull request successfully merged into master. Build succeeded: |
callesonne
pushed a commit
to callesonne/mathlib4
that referenced
this pull request
Jul 24, 2025
…er-community#27318) These can be constructed with less work via the injectivity constructors. This also adds the cancellative instances.
hrmacbeth
pushed a commit
to szqzs/mathlib4
that referenced
this pull request
Jul 28, 2025
…er-community#27318) These can be constructed with less work via the injectivity constructors. This also adds the cancellative instances.
Equilibris
pushed a commit
to Equilibris/mathlib4
that referenced
this pull request
Aug 7, 2025
…er-community#27318) These can be constructed with less work via the injectivity constructors. This also adds the cancellative instances.
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.
These can be constructed with less work via the injectivity constructors.
This also adds the cancellative instances.