chore: fix for nightly-testing by Rob23oba · Pull Request #26246 · leanprover-community/mathlib4

Rob23oba · 2025-06-21T08:22:25Z

The deletions in f030f37 seem to not have been properly merged into nightly-testing

github-actions · 2025-06-21T08:23:38Z

PR summary c3b173fdbb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
2359 files `Mathlib.Algebra.AddConstMap.Basic` `Mathlib.Algebra.AddConstMap.Equiv` `Mathlib.Algebra.AddTorsor.Defs` `Mathlib.Algebra.Algebra.Basic` `Mathlib.Algebra.Algebra.Bilinear` `Mathlib.Algebra.Algebra.Defs` `Mathlib.Algebra.Algebra.Equiv` `Mathlib.Algebra.Algebra.Field` `Mathlib.Algebra.Algebra.Hom.Rat` `Mathlib.Algebra.Algebra.Hom` `Mathlib.Algebra.Algebra.NonUnitalHom` `Mathlib.Algebra.Algebra.NonUnitalSubalgebra` `Mathlib.Algebra.Algebra.Operations` `Mathlib.Algebra.Algebra.Opposite` `Mathlib.Algebra.Algebra.Pi` `Mathlib.Algebra.Algebra.Prod` `Mathlib.Algebra.Algebra.Rat` `Mathlib.Algebra.Algebra.RestrictScalars` `Mathlib.Algebra.Algebra.Spectrum.Basic` `Mathlib.Algebra.Algebra.Spectrum.Pi` `Mathlib.Algebra.Algebra.Spectrum.Quasispectrum` `Mathlib.Algebra.Algebra.Subalgebra.Basic` `Mathlib.Algebra.Algebra.Subalgebra.Centralizer` `Mathlib.Algebra.Algebra.Subalgebra.Directed` `Mathlib.Algebra.Algebra.Subalgebra.Lattice` `Mathlib.Algebra.Algebra.Subalgebra.MulOpposite` `Mathlib.Algebra.Algebra.Subalgebra.Operations` `Mathlib.Algebra.Algebra.Subalgebra.Order` `Mathlib.Algebra.Algebra.Subalgebra.Pi` `Mathlib.Algebra.Algebra.Subalgebra.Pointwise` `Mathlib.Algebra.Algebra.Subalgebra.Prod` `Mathlib.Algebra.Algebra.Subalgebra.Tower` `Mathlib.Algebra.Algebra.Subalgebra.Unitization` `Mathlib.Algebra.Algebra.Tower` `Mathlib.Algebra.Algebra.Unitization` `Mathlib.Algebra.Azumaya.Basic` `Mathlib.Algebra.Azumaya.Defs` `Mathlib.Algebra.BigOperators.Associated` `Mathlib.Algebra.BigOperators.Balance` `Mathlib.Algebra.BigOperators.Expect` `Mathlib.Algebra.BigOperators.Field` `Mathlib.Algebra.BigOperators.Fin` `Mathlib.Algebra.BigOperators.Finprod` `Mathlib.Algebra.BigOperators.Finsupp.Basic` `Mathlib.Algebra.BigOperators.Finsupp.Fin` `Mathlib.Algebra.BigOperators.Group.List.Defs` `Mathlib.Algebra.BigOperators.GroupWithZero.Action` `Mathlib.Algebra.BigOperators.Module` `Mathlib.Algebra.BigOperators.Ring.Finset` `Mathlib.Algebra.Category.AlgCat.Basic` `Mathlib.Algebra.Category.AlgCat.Limits` `Mathlib.Algebra.Category.AlgCat.Monoidal` `Mathlib.Algebra.Category.AlgCat.Symmetric` `Mathlib.Algebra.Category.AlgebraCat.Symmetric` `Mathlib.Algebra.Category.BialgCat.Basic` `Mathlib.Algebra.Category.BialgCat.Monoidal` `Mathlib.Algebra.Category.BoolRing` `Mathlib.Algebra.Category.CoalgCat.Basic` `Mathlib.Algebra.Category.CoalgCat.ComonEquivalence` `Mathlib.Algebra.Category.CoalgCat.Monoidal` `Mathlib.Algebra.Category.Grp.Basic` `Mathlib.Algebra.Category.Grp.Biproducts` `Mathlib.Algebra.Category.Grp.CartesianMonoidal` `Mathlib.Algebra.Category.Grp.ChosenFiniteProducts` `Mathlib.Algebra.Category.Grp.Colimits` `Mathlib.Algebra.Category.Grp.EpiMono` `Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup` `Mathlib.Algebra.Category.Grp.FilteredColimits` `Mathlib.Algebra.Category.Grp.FiniteGrp` `Mathlib.Algebra.Category.Grp.ForgetCorepresentable` `Mathlib.Algebra.Category.Grp.Kernels` `Mathlib.Algebra.Category.Grp.LeftExactFunctor` `Mathlib.Algebra.Category.Grp.Limits` `Mathlib.Algebra.Category.Grp.Preadditive` `Mathlib.Algebra.Category.Grp.ZModuleEquivalence` `Mathlib.Algebra.Category.Grp.Zero` `Mathlib.Algebra.Category.HopfAlgCat.Basic` `Mathlib.Algebra.Category.HopfAlgCat.Monoidal` `Mathlib.Algebra.Category.ModuleCat.Adjunctions` `Mathlib.Algebra.Category.ModuleCat.Algebra` `Mathlib.Algebra.Category.ModuleCat.Basic` `Mathlib.Algebra.Category.ModuleCat.Colimits` `Mathlib.Algebra.Category.ModuleCat.FilteredColimits` `Mathlib.Algebra.Category.ModuleCat.Limits` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric` `Mathlib.Algebra.Category.ModuleCat.Products` `Mathlib.Algebra.Category.ModuleCat.Tannaka` `Mathlib.Algebra.Category.MonCat.Adjunctions` `Mathlib.Algebra.Category.MonCat.Limits` `Mathlib.Algebra.Category.Ring.Adjunctions` `Mathlib.Algebra.Category.Ring.Basic` `Mathlib.Algebra.Category.Ring.Colimits` `Mathlib.Algebra.Category.Ring.FilteredColimits` `Mathlib.Algebra.Category.Ring.Limits` `Mathlib.Algebra.Central.Basic` `Mathlib.Algebra.Central.Defs` `Mathlib.Algebra.Central.Matrix` `Mathlib.Algebra.CharP.Algebra` `Mathlib.Algebra.CharP.Frobenius` `Mathlib.Algebra.CharP.IntermediateField` `Mathlib.Algebra.CharP.Invertible` `Mathlib.Algebra.CharP.Lemmas` `Mathlib.Algebra.CharP.Reduced` `Mathlib.Algebra.CharP.Subring` `Mathlib.Algebra.CharZero.Defs` `Mathlib.Algebra.CharZero.Quotient` `Mathlib.Algebra.Colimit.DirectLimit` `Mathlib.Algebra.Colimit.Finiteness` `Mathlib.Algebra.Colimit.Module` `Mathlib.Algebra.Colimit.TensorProduct` `Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries` `Mathlib.Algebra.ContinuedFractions.Computation.Approximations` `Mathlib.Algebra.ContinuedFractions.Computation.Basic` `Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating` `Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat` `Mathlib.Algebra.ContinuedFractions.Computation.Translations` `Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv` `Mathlib.Algebra.ContinuedFractions.Determinant` `Mathlib.Algebra.CubicDiscriminant` `Mathlib.Algebra.DirectSum.AddChar` `Mathlib.Algebra.DirectSum.Algebra` `Mathlib.Algebra.DirectSum.Basic` `Mathlib.Algebra.DirectSum.Decomposition` `Mathlib.Algebra.DirectSum.Finsupp` `Mathlib.Algebra.DirectSum.Internal` `Mathlib.Algebra.DirectSum.Module` `Mathlib.Algebra.DirectSum.Ring` `Mathlib.Algebra.DualNumber` `Mathlib.Algebra.Equiv.TransferInstance` `Mathlib.Algebra.EuclideanDomain.Defs` `Mathlib.Algebra.EuclideanDomain.Field` `Mathlib.Algebra.Expr` `Mathlib.Algebra.Field.Basic` `Mathlib.Algebra.Field.Defs` `Mathlib.Algebra.Field.MinimalAxioms` `Mathlib.Algebra.Field.Opposite` `Mathlib.Algebra.Field.Power` `Mathlib.Algebra.Field.Rat` `Mathlib.Algebra.Field.Subfield.Basic` `Mathlib.Algebra.Field.Subfield.Defs` `Mathlib.Algebra.Field.ULift` `Mathlib.Algebra.FreeAlgebra` `Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra` `Mathlib.Algebra.Free` `Mathlib.Algebra.GCDMonoid.Nat` `Mathlib.Algebra.GeomSum` `Mathlib.Algebra.Group.Action.Basic` `Mathlib.Algebra.Group.Action.Defs` `Mathlib.Algebra.Group.Action.Faithful` `Mathlib.Algebra.Group.Action.Hom` `Mathlib.Algebra.Group.Action.Opposite` `Mathlib.Algebra.Group.Action.Option` `Mathlib.Algebra.Group.Action.Pi` `Mathlib.Algebra.Group.Action.Pointwise.Set.Basic` `Mathlib.Algebra.Group.Action.Pretransitive` `Mathlib.Algebra.Group.Action.Prod` `Mathlib.Algebra.Group.Action.Sigma` `Mathlib.Algebra.Group.Action.Sum` `Mathlib.Algebra.Group.Action.TypeTags` `Mathlib.Algebra.Group.Action.Units` `Mathlib.Algebra.Group.AddChar` `Mathlib.Algebra.Group.Basic` `Mathlib.Algebra.Group.Center` `Mathlib.Algebra.Group.Commutator` `Mathlib.Algebra.Group.Commute.Basic` `Mathlib.Algebra.Group.Commute.Defs` `Mathlib.Algebra.Group.Commute.Hom` `Mathlib.Algebra.Group.Commute.Units` `Mathlib.Algebra.Group.Defs` `Mathlib.Algebra.Group.Embedding` `Mathlib.Algebra.Group.Equiv.Basic` `Mathlib.Algebra.Group.Equiv.Defs` `Mathlib.Algebra.Group.Equiv.Opposite` `Mathlib.Algebra.Group.Equiv.TypeTags` `Mathlib.Algebra.Group.EvenFunction` `Mathlib.Algebra.Group.Even` `Mathlib.Algebra.Group.Ext` `Mathlib.Algebra.Group.ForwardDiff` `Mathlib.Algebra.Group.Hom.Basic` `Mathlib.Algebra.Group.Hom.CompTypeclasses` `Mathlib.Algebra.Group.Hom.Defs` `Mathlib.Algebra.Group.Hom.End` `Mathlib.Algebra.Group.Hom.Instances` `Mathlib.Algebra.Group.Idempotent` `Mathlib.Algebra.Group.Indicator` `Mathlib.Algebra.Group.InjSurj` `Mathlib.Algebra.Group.Int.Defs` `Mathlib.Algebra.Group.Int.TypeTags` `Mathlib.Algebra.Group.Int.Units` `Mathlib.Algebra.Group.Invertible.Basic` `Mathlib.Algebra.Group.Invertible.Defs` `Mathlib.Algebra.Group.Irreducible.Defs` `Mathlib.Algebra.Group.Irreducible.Lemmas` `Mathlib.Algebra.Group.MinimalAxioms` `Mathlib.Algebra.Group.Nat.Defs` `Mathlib.Algebra.Group.Nat.Even` `Mathlib.Algebra.Group.Nat.Hom` `Mathlib.Algebra.Group.Nat.TypeTags` `Mathlib.Algebra.Group.Nat.Units` `Mathlib.Algebra.Group.NatPowAssoc` `Mathlib.Algebra.Group.Opposite` `Mathlib.Algebra.Group.PUnit` `Mathlib.Algebra.Group.Pi.Basic` `Mathlib.Algebra.Group.Pi.Lemmas` `Mathlib.Algebra.Group.Pi.Units` `Mathlib.Algebra.Group.Pointwise.Finset.Density` `Mathlib.Algebra.Group.Pointwise.Finset.Interval` `Mathlib.Algebra.Group.Pointwise.Set.Basic` `Mathlib.Algebra.Group.Pointwise.Set.Lattice` `Mathlib.Algebra.Group.Pointwise.Set.Scalar` `Mathlib.Algebra.Group.Prod` `Mathlib.Algebra.Group.Semiconj.Basic` `Mathlib.Algebra.Group.Semiconj.Defs` `Mathlib.Algebra.Group.Semiconj.Units` `Mathlib.Algebra.Group.Subgroup.Finsupp` `Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas` `Mathlib.Algebra.Group.Submonoid.Basic` `Mathlib.Algebra.Group.Submonoid.Defs` `Mathlib.Algebra.Group.Submonoid.DistribMulAction` `Mathlib.Algebra.Group.Submonoid.Finsupp` `Mathlib.Algebra.Group.Submonoid.MulAction` `Mathlib.Algebra.Group.Submonoid.MulOpposite` `Mathlib.Algebra.Group.Submonoid.Operations` `Mathlib.Algebra.Group.Subsemigroup.Basic` `Mathlib.Algebra.Group.Subsemigroup.Defs` `Mathlib.Algebra.Group.Subsemigroup.Membership` `Mathlib.Algebra.Group.Subsemigroup.Operations` `Mathlib.Algebra.Group.Support` `Mathlib.Algebra.Group.Torsion` `Mathlib.Algebra.Group.TypeTags.Basic` `Mathlib.Algebra.Group.TypeTags.Hom` `Mathlib.Algebra.Group.ULift` `Mathlib.Algebra.Group.Units.Basic` `Mathlib.Algebra.Group.Units.Defs` `Mathlib.Algebra.Group.Units.Equiv` `Mathlib.Algebra.Group.Units.Hom` `Mathlib.Algebra.Group.Units.Opposite` `Mathlib.Algebra.GroupWithZero.Action.Defs` `Mathlib.Algebra.GroupWithZero.Action.End` `Mathlib.Algebra.GroupWithZero.Action.Faithful` `Mathlib.Algebra.GroupWithZero.Action.Opposite` `Mathlib.Algebra.GroupWithZero.Action.Prod` `Mathlib.Algebra.GroupWithZero.Action.Units` `Mathlib.Algebra.GroupWithZero.Basic` `Mathlib.Algebra.GroupWithZero.Center` `Mathlib.Algebra.GroupWithZero.Commute` `Mathlib.Algebra.GroupWithZero.Defs` `Mathlib.Algebra.GroupWithZero.Equiv` `Mathlib.Algebra.GroupWithZero.Hom` `Mathlib.Algebra.GroupWithZero.Idempotent` `Mathlib.Algebra.GroupWithZero.Indicator` `Mathlib.Algebra.GroupWithZero.InjSurj` `Mathlib.Algebra.GroupWithZero.Invertible` `Mathlib.Algebra.GroupWithZero.Nat` `Mathlib.Algebra.GroupWithZero.NeZero` `Mathlib.Algebra.GroupWithZero.Opposite` `Mathlib.Algebra.GroupWithZero.Pi` `Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic` `Mathlib.Algebra.GroupWithZero.Semiconj` `Mathlib.Algebra.GroupWithZero.ULift` `Mathlib.Algebra.GroupWithZero.Units.Basic` `Mathlib.Algebra.GroupWithZero.Units.Equiv` `Mathlib.Algebra.GroupWithZero.Units.Lemmas` `Mathlib.Algebra.HierarchyDesign` `Mathlib.Algebra.Homology.Additive` `Mathlib.Algebra.Homology.AlternatingConst` `Mathlib.Algebra.Homology.Augment` `Mathlib.Algebra.Homology.CommSq` `Mathlib.Algebra.Homology.ComplexShape` `Mathlib.Algebra.Homology.DifferentialObject` `Mathlib.Algebra.Homology.Double` `Mathlib.Algebra.Homology.Embedding.Boundary` `Mathlib.Algebra.Homology.Embedding.Connect` `Mathlib.Algebra.Homology.Embedding.ExtendHomology` `Mathlib.Algebra.Homology.Embedding.Extend` `Mathlib.Algebra.Homology.Embedding.HomEquiv` `Mathlib.Algebra.Homology.Embedding.IsSupported` `Mathlib.Algebra.Homology.Embedding.RestrictionHomology` `Mathlib.Algebra.Homology.Embedding.Restriction` `Mathlib.Algebra.Homology.Embedding.StupidTrunc` `Mathlib.Algebra.Homology.Embedding.TruncGEHomology` `Mathlib.Algebra.Homology.Embedding.TruncGE` `Mathlib.Algebra.Homology.Embedding.TruncLEHomology` `Mathlib.Algebra.Homology.Embedding.TruncLE` `Mathlib.Algebra.Homology.ExactSequence` `Mathlib.Algebra.Homology.Factorizations.Basic` `Mathlib.Algebra.Homology.Functor` `Mathlib.Algebra.Homology.GrothendieckAbelian` `Mathlib.Algebra.Homology.HasNoLoop` `Mathlib.Algebra.Homology.HomologicalBicomplex` `Mathlib.Algebra.Homology.HomologicalComplexAbelian` `Mathlib.Algebra.Homology.HomologicalComplexBiprod` `Mathlib.Algebra.Homology.HomologicalComplexLimits` `Mathlib.Algebra.Homology.HomologicalComplex` `Mathlib.Algebra.Homology.HomologySequenceLemmas` `Mathlib.Algebra.Homology.HomologySequence` `Mathlib.Algebra.Homology.HomotopyCategory` `Mathlib.Algebra.Homology.HomotopyCofiber` `Mathlib.Algebra.Homology.Homotopy` `Mathlib.Algebra.Homology.ImageToKernel` `Mathlib.Algebra.Homology.Linear` `Mathlib.Algebra.Homology.Localization` `Mathlib.Algebra.Homology.Opposite` `Mathlib.Algebra.Homology.QuasiIso` `Mathlib.Algebra.Homology.Refinements` `Mathlib.Algebra.Homology.ShortComplex.Abelian` `Mathlib.Algebra.Homology.ShortComplex.ExactFunctor` `Mathlib.Algebra.Homology.ShortComplex.Exact` `Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex` `Mathlib.Algebra.Homology.ShortComplex.Linear` `Mathlib.Algebra.Homology.ShortComplex.Preadditive` `Mathlib.Algebra.Homology.ShortComplex.ShortExact` `Mathlib.Algebra.Homology.ShortComplex.SnakeLemma` `Mathlib.Algebra.Homology.SingleHomology` `Mathlib.Algebra.Homology.Single` `Mathlib.Algebra.Homology.Square` `Mathlib.Algebra.Lie.Basic` `Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra` `Mathlib.Algebra.ModEq` `Mathlib.Algebra.Module.Basic` `Mathlib.Algebra.Module.BigOperators` `Mathlib.Algebra.Module.Bimodule` `Mathlib.Algebra.Module.Card` `Mathlib.Algebra.Module.Defs` `Mathlib.Algebra.Module.End` `Mathlib.Algebra.Module.Equiv.Basic` `Mathlib.Algebra.Module.Equiv.Defs` `Mathlib.Algebra.Module.Equiv.Opposite` `Mathlib.Algebra.Module.GradedModule` `Mathlib.Algebra.Module.Hom` `Mathlib.Algebra.Module.Injective` `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.LocalizedModule.AtPrime` `Mathlib.Algebra.Module.LocalizedModule.Away` `Mathlib.Algebra.Module.LocalizedModule.Basic` `Mathlib.Algebra.Module.LocalizedModule.Int` `Mathlib.Algebra.Module.LocalizedModule.IsLocalization` `Mathlib.Algebra.Module.MinimalAxioms` `Mathlib.Algebra.Module.NatInt` `Mathlib.Algebra.Module.Opposite` `Mathlib.Algebra.Module.PUnit` `Mathlib.Algebra.Module.PointwisePi` `Mathlib.Algebra.Module.Prod` `Mathlib.Algebra.Module.Projective` `Mathlib.Algebra.Module.Rat` `Mathlib.Algebra.Module.RingHom` `Mathlib.Algebra.Module.Submodule.Bilinear` `Mathlib.Algebra.Module.Submodule.EqLocus` `Mathlib.Algebra.Module.Submodule.Equiv` `Mathlib.Algebra.Module.Submodule.Invariant` `Mathlib.Algebra.Module.Submodule.IterateMapComap` `Mathlib.Algebra.Module.Submodule.Ker` `Mathlib.Algebra.Module.Submodule.Lattice` `Mathlib.Algebra.Module.Submodule.LinearMap` `Mathlib.Algebra.Module.Submodule.Map` `Mathlib.Algebra.Module.Submodule.Pointwise` `Mathlib.Algebra.Module.Submodule.Range` `Mathlib.Algebra.Module.Submodule.RestrictScalars` `Mathlib.Algebra.Module.ULift` `Mathlib.Algebra.MonoidAlgebra.Basic` `Mathlib.Algebra.MonoidAlgebra.Defs` `Mathlib.Algebra.MonoidAlgebra.Degree` `Mathlib.Algebra.MonoidAlgebra.Division` `Mathlib.Algebra.MonoidAlgebra.Grading` `Mathlib.Algebra.MonoidAlgebra.Ideal` `Mathlib.Algebra.MonoidAlgebra.MapDomain` `Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors` `Mathlib.Algebra.MonoidAlgebra.Support` `Mathlib.Algebra.MonoidAlgebra.ToDirectSum` `Mathlib.Algebra.MvPolynomial.Basic` `Mathlib.Algebra.MvPolynomial.Cardinal` `Mathlib.Algebra.MvPolynomial.Comap` `Mathlib.Algebra.MvPolynomial.CommRing` `Mathlib.Algebra.MvPolynomial.Counit` `Mathlib.Algebra.MvPolynomial.Degrees` `Mathlib.Algebra.MvPolynomial.Derivation` `Mathlib.Algebra.MvPolynomial.Division` `Mathlib.Algebra.MvPolynomial.Equiv` `Mathlib.Algebra.MvPolynomial.Eval` `Mathlib.Algebra.MvPolynomial.Expand` `Mathlib.Algebra.MvPolynomial.Invertible` `Mathlib.Algebra.MvPolynomial.Monad` `Mathlib.Algebra.MvPolynomial.PDeriv` `Mathlib.Algebra.MvPolynomial.Polynomial` `Mathlib.Algebra.MvPolynomial.Rename` `Mathlib.Algebra.MvPolynomial.SchwartzZippel` `Mathlib.Algebra.MvPolynomial.Supported` `Mathlib.Algebra.MvPolynomial.Variables` `Mathlib.Algebra.NeZero` `Mathlib.Algebra.NoZeroSMulDivisors.Basic` `Mathlib.Algebra.NoZeroSMulDivisors.Defs` `Mathlib.Algebra.NoZeroSMulDivisors.Pi` `Mathlib.Algebra.NoZeroSMulDivisors.Prod` `Mathlib.Algebra.Notation.Defs` `Mathlib.Algebra.Notation.Lemmas` `Mathlib.Algebra.Notation.Pi` `Mathlib.Algebra.Notation.Prod` `Mathlib.Algebra.Notation` `Mathlib.Algebra.Opposites` `Mathlib.Algebra.Order.AbsoluteValue.Basic` `Mathlib.Algebra.Order.AbsoluteValue.Euclidean` `Mathlib.Algebra.Order.AddGroupWithTop` `Mathlib.Algebra.Order.AddTorsor` `Mathlib.Algebra.Order.Algebra` `Mathlib.Algebra.Order.Antidiag.Finsupp` `Mathlib.Algebra.Order.Antidiag.Nat` `Mathlib.Algebra.Order.Antidiag.Pi` `Mathlib.Algebra.Order.Archimedean.Basic` `Mathlib.Algebra.Order.Archimedean.Class` `Mathlib.Algebra.Order.Archimedean.Hom` `Mathlib.Algebra.Order.Archimedean.Submonoid` `Mathlib.Algebra.Order.BigOperators.Expect` `Mathlib.Algebra.Order.BigOperators.GroupWithZero.List` `Mathlib.Algebra.Order.BigOperators.Ring.Finset` `Mathlib.Algebra.Order.CauSeq.Basic` `Mathlib.Algebra.Order.CauSeq.BigOperators` `Mathlib.Algebra.Order.CauSeq.Completion` `Mathlib.Algebra.Order.CompleteField` `Mathlib.Algebra.Order.Field.Basic` `Mathlib.Algebra.Order.Field.Defs` `Mathlib.Algebra.Order.Field.InjSurj` `Mathlib.Algebra.Order.Field.Pointwise` `Mathlib.Algebra.Order.Field.Power` `Mathlib.Algebra.Order.Field.Rat` `Mathlib.Algebra.Order.Field.Subfield` `Mathlib.Algebra.Order.Floor.Defs` `Mathlib.Algebra.Order.Floor.Div` `Mathlib.Algebra.Order.Floor.Ring` `Mathlib.Algebra.Order.Floor.Semiring` `Mathlib.Algebra.Order.Floor` `Mathlib.Algebra.Order.Group.Abs` `Mathlib.Algebra.Order.Group.Action.End` `Mathlib.Algebra.Order.Group.Action.Flag` `Mathlib.Algebra.Order.Group.Action.Synonym` `Mathlib.Algebra.Order.Group.Action` `Mathlib.Algebra.Order.Group.Basic` `Mathlib.Algebra.Order.Group.Bounds` `Mathlib.Algebra.Order.Group.CompleteLattice` `Mathlib.Algebra.Order.Group.Cone` `Mathlib.Algebra.Order.Group.Defs` `Mathlib.Algebra.Order.Group.DenselyOrdered` `Mathlib.Algebra.Order.Group.End` `Mathlib.Algebra.Order.Group.Indicator` `Mathlib.Algebra.Order.Group.InjSurj` `Mathlib.Algebra.Order.Group.Instances` `Mathlib.Algebra.Order.Group.Int.Sum` `Mathlib.Algebra.Order.Group.Int` `Mathlib.Algebra.Order.Group.Lattice` `Mathlib.Algebra.Order.Group.MinMax` `Mathlib.Algebra.Order.Group.Nat` `Mathlib.Algebra.Order.Group.Opposite` `Mathlib.Algebra.Order.Group.OrderIso` `Mathlib.Algebra.Order.Group.Pointwise.Bounds` `Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice` `Mathlib.Algebra.Order.Group.Pointwise.Interval` `Mathlib.Algebra.Order.Group.PosPart` `Mathlib.Algebra.Order.Group.Prod` `Mathlib.Algebra.Order.Group.Synonym` `Mathlib.Algebra.Order.Group.TypeTags` `Mathlib.Algebra.Order.Group.Unbundled.Abs` `Mathlib.Algebra.Order.Group.Unbundled.Basic` `Mathlib.Algebra.Order.Group.Unbundled.Int` `Mathlib.Algebra.Order.Group.Units` `Mathlib.Algebra.Order.GroupWithZero.Bounds` `Mathlib.Algebra.Order.GroupWithZero.Submonoid` `Mathlib.Algebra.Order.GroupWithZero.Synonym` `Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic` `Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs` `Mathlib.Algebra.Order.GroupWithZero.Unbundled.Lemmas` `Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso` `Mathlib.Algebra.Order.GroupWithZero.Unbundled` `Mathlib.Algebra.Order.Hom.Basic` `Mathlib.Algebra.Order.Interval.Basic` `Mathlib.Algebra.Order.Interval.Set.Group` `Mathlib.Algebra.Order.Interval.Set.Instances` `Mathlib.Algebra.Order.Interval.Set.Monoid` `Mathlib.Algebra.Order.Module.Algebra` `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.Module.Rat` `Mathlib.Algebra.Order.Monoid.Basic` `Mathlib.Algebra.Order.Monoid.Canonical.Defs` `Mathlib.Algebra.Order.Monoid.Defs` `Mathlib.Algebra.Order.Monoid.NatCast` `Mathlib.Algebra.Order.Monoid.OrderDual` `Mathlib.Algebra.Order.Monoid.Prod` `Mathlib.Algebra.Order.Monoid.Submonoid` `Mathlib.Algebra.Order.Monoid.TypeTags` `Mathlib.Algebra.Order.Monoid.Unbundled.Basic` `Mathlib.Algebra.Order.Monoid.Unbundled.Defs` `Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE` `Mathlib.Algebra.Order.Monoid.Unbundled.MinMax` `Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual` `Mathlib.Algebra.Order.Monoid.Unbundled.Pow` `Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags` `Mathlib.Algebra.Order.Monoid.Unbundled.WithTop` `Mathlib.Algebra.Order.Monoid.Units` `Mathlib.Algebra.Order.Monoid.WithTop` `Mathlib.Algebra.Order.Monovary` `Mathlib.Algebra.Order.Nonneg.Floor` `Mathlib.Algebra.Order.Nonneg.Module` `Mathlib.Algebra.Order.PUnit` `Mathlib.Algebra.Order.Pi` `Mathlib.Algebra.Order.Positive.Field` `Mathlib.Algebra.Order.Positive.Ring` `Mathlib.Algebra.Order.Quantale` `Mathlib.Algebra.Order.Rearrangement` `Mathlib.Algebra.Order.Ring.Abs` `Mathlib.Algebra.Order.Ring.Cast` `Mathlib.Algebra.Order.Ring.Cone` `Mathlib.Algebra.Order.Ring.Defs` `Mathlib.Algebra.Order.Ring.Idempotent` `Mathlib.Algebra.Order.Ring.InjSurj` `Mathlib.Algebra.Order.Ring.Int` `Mathlib.Algebra.Order.Ring.IsNonarchimedean` `Mathlib.Algebra.Order.Ring.Opposite` `Mathlib.Algebra.Order.Ring.Rat` `Mathlib.Algebra.Order.Ring.Star` `Mathlib.Algebra.Order.Ring.Synonym` `Mathlib.Algebra.Order.Ring.Unbundled.Basic` `Mathlib.Algebra.Order.Ring.Unbundled.Rat` `Mathlib.Algebra.Order.Round` `Mathlib.Algebra.Order.Star.Basic` `Mathlib.Algebra.Order.Star.Conjneg` `Mathlib.Algebra.Order.Star.Prod` `Mathlib.Algebra.Order.Sub.Basic` `Mathlib.Algebra.Order.Sub.Defs` `Mathlib.Algebra.Order.Sub.Prod` `Mathlib.Algebra.Order.Sub.Unbundled.Basic` `Mathlib.Algebra.Order.Sub.Unbundled.Hom` `Mathlib.Algebra.Order.Sub.WithTop` `Mathlib.Algebra.Order.Sum` `Mathlib.Algebra.Order.ZeroLEOne` `Mathlib.Algebra.PEmptyInstances` `Mathlib.Algebra.Polynomial.AlgebraMap` `Mathlib.Algebra.Polynomial.Basic` `Mathlib.Algebra.Polynomial.Basis` `Mathlib.Algebra.Polynomial.BigOperators` `Mathlib.Algebra.Polynomial.CancelLeads` `Mathlib.Algebra.Polynomial.Cardinal` `Mathlib.Algebra.Polynomial.CoeffList` `Mathlib.Algebra.Polynomial.CoeffMem` `Mathlib.Algebra.Polynomial.Coeff` `Mathlib.Algebra.Polynomial.Degree.CardPowDegree` `Mathlib.Algebra.Polynomial.Degree.Definitions` `Mathlib.Algebra.Polynomial.Degree.Domain` `Mathlib.Algebra.Polynomial.Degree.Lemmas` `Mathlib.Algebra.Polynomial.Degree.Monomial` `Mathlib.Algebra.Polynomial.Degree.Operations` `Mathlib.Algebra.Polynomial.Degree.SmallDegree` `Mathlib.Algebra.Polynomial.Degree.Support` `Mathlib.Algebra.Polynomial.Degree.TrailingDegree` `Mathlib.Algebra.Polynomial.Degree.Units` `Mathlib.Algebra.Polynomial.DenomsClearable` `Mathlib.Algebra.Polynomial.Derivation` `Mathlib.Algebra.Polynomial.Derivative` `Mathlib.Algebra.Polynomial.Div` `Mathlib.Algebra.Polynomial.EraseLead` `Mathlib.Algebra.Polynomial.Eval.Algebra` `Mathlib.Algebra.Polynomial.Eval.Coeff` `Mathlib.Algebra.Polynomial.Eval.Defs` `Mathlib.Algebra.Polynomial.Eval.Degree` `Mathlib.Algebra.Polynomial.Eval.Irreducible` `Mathlib.Algebra.Polynomial.Eval.SMul` `Mathlib.Algebra.Polynomial.Eval.Subring` `Mathlib.Algebra.Polynomial.FieldDivision` `Mathlib.Algebra.Polynomial.GroupRingAction` `Mathlib.Algebra.Polynomial.HasseDeriv` `Mathlib.Algebra.Polynomial.Identities` `Mathlib.Algebra.Polynomial.Inductions` `Mathlib.Algebra.Polynomial.Laurent` `Mathlib.Algebra.Polynomial.Lifts` `Mathlib.Algebra.Polynomial.Mirror` `Mathlib.Algebra.Polynomial.Module.AEval` `Mathlib.Algebra.Polynomial.Module.Basic` `Mathlib.Algebra.Polynomial.Monic` `Mathlib.Algebra.Polynomial.Monomial` `Mathlib.Algebra.Polynomial.OfFn` `Mathlib.Algebra.Polynomial.PartialFractions` `Mathlib.Algebra.Polynomial.Reverse` `Mathlib.Algebra.Polynomial.RingDivision` `Mathlib.Algebra.Polynomial.Roots` `Mathlib.Algebra.Polynomial.Sequence` `Mathlib.Algebra.Polynomial.Smeval` `Mathlib.Algebra.Polynomial.SpecificDegree` `Mathlib.Algebra.Polynomial.Splits` `Mathlib.Algebra.Polynomial.SumIteratedDerivative` `Mathlib.Algebra.Polynomial.Taylor` `Mathlib.Algebra.Polynomial.UnitTrinomial` `Mathlib.Algebra.QuadraticDiscriminant` `Mathlib.Algebra.Regular.Basic` `Mathlib.Algebra.Regular.Opposite` `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.Field` `Mathlib.Algebra.Ring.Action.Pointwise.Set` `Mathlib.Algebra.Ring.Action.Rat` `Mathlib.Algebra.Ring.Associator` `Mathlib.Algebra.Ring.Basic` `Mathlib.Algebra.Ring.BooleanRing` `Mathlib.Algebra.Ring.Center` `Mathlib.Algebra.Ring.Centralizer` `Mathlib.Algebra.Ring.CentroidHom` `Mathlib.Algebra.Ring.Commute` `Mathlib.Algebra.Ring.CompTypeclasses` `Mathlib.Algebra.Ring.Defs` `Mathlib.Algebra.Ring.Divisibility.Lemmas` `Mathlib.Algebra.Ring.Equiv` `Mathlib.Algebra.Ring.Ext` `Mathlib.Algebra.Ring.GrindInstances` `Mathlib.Algebra.Ring.Hom.Basic` `Mathlib.Algebra.Ring.Hom.Defs` `Mathlib.Algebra.Ring.Hom.InjSurj` `Mathlib.Algebra.Ring.Idempotent` `Mathlib.Algebra.Ring.Identities` `Mathlib.Algebra.Ring.InjSurj` `Mathlib.Algebra.Ring.Int.Parity` `Mathlib.Algebra.Ring.Invertible` `Mathlib.Algebra.Ring.MinimalAxioms` `Mathlib.Algebra.Ring.Nat` `Mathlib.Algebra.Ring.Opposite` `Mathlib.Algebra.Ring.PUnit` `Mathlib.Algebra.Ring.Pi` `Mathlib.Algebra.Ring.Pointwise.Set` `Mathlib.Algebra.Ring.Rat` `Mathlib.Algebra.Ring.Regular` `Mathlib.Algebra.Ring.Semiconj` `Mathlib.Algebra.Ring.Semireal.Defs` `Mathlib.Algebra.Ring.Submonoid.Basic` `Mathlib.Algebra.Ring.Submonoid` `Mathlib.Algebra.Ring.Subring.Basic` `Mathlib.Algebra.Ring.Subring.IntPolynomial` `Mathlib.Algebra.Ring.Subring.MulOpposite` `Mathlib.Algebra.Ring.Subring.Pointwise` `Mathlib.Algebra.Ring.Subsemiring.Basic` `Mathlib.Algebra.Ring.Subsemiring.Defs` `Mathlib.Algebra.Ring.Subsemiring.MulOpposite` `Mathlib.Algebra.Ring.Subsemiring.Order` `Mathlib.Algebra.Ring.Subsemiring.Pointwise` `Mathlib.Algebra.Ring.SumsOfSquares` `Mathlib.Algebra.Ring.ULift` `Mathlib.Algebra.Ring.Units` `Mathlib.Algebra.RingQuot` `Mathlib.Algebra.SkewMonoidAlgebra.Basic` `Mathlib.Algebra.Small.Group` `Mathlib.Algebra.Small.Module` `Mathlib.Algebra.Small.Ring` `Mathlib.Algebra.Squarefree.Basic` `Mathlib.Algebra.Star.Basic` `Mathlib.Algebra.Star.BigOperators` `Mathlib.Algebra.Star.Center` `Mathlib.Algebra.Star.CentroidHom` `Mathlib.Algebra.Star.Conjneg` `Mathlib.Algebra.Star.Free` `Mathlib.Algebra.Star.Module` `Mathlib.Algebra.Star.NonUnitalSubalgebra` `Mathlib.Algebra.Star.NonUnitalSubsemiring` `Mathlib.Algebra.Star.Pi` `Mathlib.Algebra.Star.Pointwise` `Mathlib.Algebra.Star.Prod` `Mathlib.Algebra.Star.Rat` `Mathlib.Algebra.Star.RingQuot` `Mathlib.Algebra.Star.SelfAdjoint` `Mathlib.Algebra.Star.StarAlgHom` `Mathlib.Algebra.Star.StarRingHom` `Mathlib.Algebra.Star.Subalgebra` `Mathlib.Algebra.Star.Subsemiring` `Mathlib.Algebra.Star.Unitary` `Mathlib.Algebra.TrivSqZeroExt` `Mathlib.Algebra.Tropical.Basic` `Mathlib.Algebra.Tropical.Lattice` `Mathlib.Algebra.Vertex.HVertexOperator` `Mathlib.Algebra.Vertex.VertexOperator` `Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ` `Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms` `Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange` `Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology` `Mathlib.AlgebraicTopology.AlternatingFaceMapComplex` `Mathlib.AlgebraicTopology.CechNerve` `Mathlib.AlgebraicTopology.DoldKan.Decomposition` `Mathlib.AlgebraicTopology.DoldKan.Degeneracies` `Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive` `Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian` `Mathlib.AlgebraicTopology.DoldKan.Equivalence` `Mathlib.AlgebraicTopology.DoldKan.Faces` `Mathlib.AlgebraicTopology.DoldKan.FunctorGamma` `Mathlib.AlgebraicTopology.DoldKan.FunctorN` `Mathlib.AlgebraicTopology.DoldKan.GammaCompN` `Mathlib.AlgebraicTopology.DoldKan.Homotopies` `Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence` `Mathlib.AlgebraicTopology.DoldKan.NCompGamma` `Mathlib.AlgebraicTopology.DoldKan.NReflectsIso` `Mathlib.AlgebraicTopology.DoldKan.Normalized` `Mathlib.AlgebraicTopology.DoldKan.Notations` `Mathlib.AlgebraicTopology.DoldKan.PInfty` `Mathlib.AlgebraicTopology.DoldKan.Projections` `Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject` `Mathlib.AlgebraicTopology.ExtraDegeneracy` `Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic` `Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup` `Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps` `Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit` `Mathlib.AlgebraicTopology.FundamentalGroupoid.Product` `Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected` `Mathlib.AlgebraicTopology.MooreComplex` `Mathlib.AlgebraicTopology.Quasicategory.Basic` `Mathlib.AlgebraicTopology.Quasicategory.Nerve` `Mathlib.AlgebraicTopology.Quasicategory.StrictSegal` `Mathlib.AlgebraicTopology.SimplexCategory.Augmented` `Mathlib.AlgebraicTopology.SimplexCategory.Basic` `Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic` `Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono` `Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms` `Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty` `Mathlib.AlgebraicTopology.SimplicialCategory.Basic` `Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject` `Mathlib.AlgebraicTopology.SimplicialNerve` `Mathlib.AlgebraicTopology.SimplicialObject.Basic` `Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal` `Mathlib.AlgebraicTopology.SimplicialObject.Split` `Mathlib.AlgebraicTopology.SimplicialSet.Basic` `Mathlib.AlgebraicTopology.SimplicialSet.Boundary` `Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations` `Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal` `Mathlib.AlgebraicTopology.SimplicialSet.Degenerate` `Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat` `Mathlib.AlgebraicTopology.SimplicialSet.Horn` `Mathlib.AlgebraicTopology.SimplicialSet.KanComplex` `Mathlib.AlgebraicTopology.SimplicialSet.Monoidal` `Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction` `Mathlib.AlgebraicTopology.SimplicialSet.Nerve` `Mathlib.AlgebraicTopology.SimplicialSet.Path` `Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex` `Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal` `Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex` `Mathlib.AlgebraicTopology.SingularHomology.Basic` `Mathlib.AlgebraicTopology.SingularSet` `Mathlib.AlgebraicTopology.TopologicalSimplex` `Mathlib.Analysis.Asymptotics.Defs` `Mathlib.Analysis.BoxIntegral.Box.Basic` `Mathlib.Analysis.BoxIntegral.Partition.Basic` `Mathlib.Analysis.BoxIntegral.Partition.Split` `Mathlib.Analysis.BoxIntegral.Partition.Tagged` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Note` `Mathlib.Analysis.Convex.Basic` `Mathlib.Analysis.Convex.Cone.Closure` `Mathlib.Analysis.Convex.Cone.Extension` `Mathlib.Analysis.Convex.Contractible` `Mathlib.Analysis.Convex.Extrema` `Mathlib.Analysis.Convex.Extreme` `Mathlib.Analysis.Convex.Function` `Mathlib.Analysis.Convex.Hull` `Mathlib.Analysis.Convex.Join` `Mathlib.Analysis.Convex.Mul` `Mathlib.Analysis.Convex.Piecewise` `Mathlib.Analysis.Convex.Quasiconvex` `Mathlib.Analysis.Convex.Segment` `Mathlib.Analysis.Convex.Slope` `Mathlib.Analysis.Convex.Star` `Mathlib.Analysis.Convex.Strict` `Mathlib.Analysis.Normed.Field.Basic` `Mathlib.Analysis.Normed.Group.AddTorsor` `Mathlib.Analysis.Normed.Group.Basic` `Mathlib.Analysis.Normed.Group.Bounded` `Mathlib.Analysis.Normed.Group.CocompactMap` `Mathlib.Analysis.Normed.Group.Constructions` `Mathlib.Analysis.Normed.Group.Continuity` `Mathlib.Analysis.Normed.Group.Int` `Mathlib.Analysis.Normed.Group.Rat` `Mathlib.Analysis.Normed.Group.Seminorm` `Mathlib.Analysis.Normed.Group.Subgroup` `Mathlib.Analysis.Normed.Group.Submodule` `Mathlib.Analysis.Normed.Lp.WithLp` `Mathlib.Analysis.Normed.Order.Basic` `Mathlib.Analysis.Normed.Order.Hom.Basic` `Mathlib.Analysis.Normed.Order.Hom.Ultra` `Mathlib.Analysis.Normed.Ring.Basic` `Mathlib.Analysis.Normed.Ring.WithAbs` `Mathlib.Analysis.NormedSpace.IndicatorFunction` `Mathlib.Analysis.NormedSpace.MStructure` `Mathlib.Analysis.Oscillation` `Mathlib.Analysis.Polynomial.CauchyBound` `Mathlib.Analysis.Subadditive` `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.Indization` `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.Indization` `Mathlib.CategoryTheory.Abelian.Injective.Resolution` `Mathlib.CategoryTheory.Abelian.LeftDerived` `Mathlib.CategoryTheory.Abelian.Monomorphisms` `Mathlib.CategoryTheory.Abelian.NonPreadditive` `Mathlib.CategoryTheory.Abelian.Opposite` `Mathlib.CategoryTheory.Abelian.Projective.Resolution` `Mathlib.CategoryTheory.Abelian.Refinements` `Mathlib.CategoryTheory.Abelian.RightDerived` `Mathlib.CategoryTheory.Abelian.SerreClass.Basic` `Mathlib.CategoryTheory.Abelian.Subobject` `Mathlib.CategoryTheory.Abelian.Transfer` `Mathlib.CategoryTheory.Action.Basic` `Mathlib.CategoryTheory.Action.Concrete` `Mathlib.CategoryTheory.Action.Continuous` `Mathlib.CategoryTheory.Action.Limits` `Mathlib.CategoryTheory.Action.Monoidal` `Mathlib.CategoryTheory.Adjunction.Additive` `Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems` `Mathlib.CategoryTheory.Category.Cat.Colimit` `Mathlib.CategoryTheory.Category.Init` `Mathlib.CategoryTheory.Center.Linear` `Mathlib.CategoryTheory.Center.Localization` `Mathlib.CategoryTheory.ConcreteCategory.Bundled` `Mathlib.CategoryTheory.Dialectica.Monoidal` `Mathlib.CategoryTheory.Distributive.Cartesian` `Mathlib.CategoryTheory.Distributive.Monoidal` `Mathlib.CategoryTheory.Generator.Abelian` `Mathlib.CategoryTheory.Generator.Basic` `Mathlib.CategoryTheory.Generator.HomologicalComplex` `Mathlib.CategoryTheory.Generator.Indization` `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.Idempotents.SimplicialObject` `Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures` `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.Cartesian.CommGrp_` `Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_` `Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_` `Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_` `Mathlib.CategoryTheory.Monoidal.CommGrp_` `Mathlib.CategoryTheory.Monoidal.Grp_` `Mathlib.CategoryTheory.Monoidal.Internal.Module` `Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_` `Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp_` `Mathlib.CategoryTheory.Monoidal.Linear` `Mathlib.CategoryTheory.Monoidal.Preadditive` `Mathlib.CategoryTheory.Monoidal.Subcategory` `Mathlib.CategoryTheory.Monoidal.Tor` `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.CommGrp_` `Mathlib.CategoryTheory.Preadditive.EilenbergMoore` `Mathlib.CategoryTheory.Preadditive.EndoFunctor` `Mathlib.CategoryTheory.Preadditive.FunctorCategory` `Mathlib.CategoryTheory.Preadditive.Indization` `Mathlib.CategoryTheory.Preadditive.Injective.Resolution` `Mathlib.CategoryTheory.Preadditive.LeftExact` `Mathlib.CategoryTheory.Preadditive.LiftToFinset` `Mathlib.CategoryTheory.Preadditive.Mat` `Mathlib.CategoryTheory.Preadditive.Opposite` `Mathlib.CategoryTheory.Preadditive.Projective.Resolution` `Mathlib.CategoryTheory.Preadditive.SingleObj` `Mathlib.CategoryTheory.Preadditive.Transfer` `Mathlib.CategoryTheory.Preadditive.Yoneda.Basic` `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.Subobject.FactorThru` `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.CovBySMul` `Mathlib.Combinatorics.Additive.DoublingConst` `Mathlib.Combinatorics.Additive.Energy` `Mathlib.Combinatorics.Additive.PluenneckeRuzsa` `Mathlib.Combinatorics.Additive.SmallTripling` `Mathlib.Combinatorics.Colex` `Mathlib.Combinatorics.Derangements.Basic` `Mathlib.Combinatorics.Derangements.Finite` `Mathlib.Combinatorics.Enumerative.Bell` `Mathlib.Combinatorics.Enumerative.Catalan` `Mathlib.Combinatorics.Enumerative.Composition` `Mathlib.Combinatorics.Enumerative.DoubleCounting` `Mathlib.Combinatorics.Enumerative.DyckWord` `Mathlib.Combinatorics.Enumerative.IncidenceAlgebra` `Mathlib.Combinatorics.Enumerative.InclusionExclusion` `Mathlib.Combinatorics.Enumerative.Partition` `Mathlib.Combinatorics.Nullstellensatz` `Mathlib.Combinatorics.Optimization.ValuedCSP` `Mathlib.Combinatorics.Pigeonhole` `Mathlib.Combinatorics.Quiver.Arborescence` `Mathlib.Combinatorics.Quiver.Basic` `Mathlib.Combinatorics.Quiver.Cast` `Mathlib.Combinatorics.Quiver.ConnectedComponent` `Mathlib.Combinatorics.Quiver.Path` `Mathlib.Combinatorics.Quiver.Prefunctor` `Mathlib.Combinatorics.Quiver.Push` `Mathlib.Combinatorics.Quiver.SingleObj` `Mathlib.Combinatorics.Quiver.Subquiver` `Mathlib.Combinatorics.Quiver.Symmetric` `Mathlib.Combinatorics.Schnirelmann` `Mathlib.Combinatorics.SetFamily.AhlswedeZhang` `Mathlib.Combinatorics.SetFamily.Compression.UV` `Mathlib.Combinatorics.SetFamily.FourFunctions` `Mathlib.Combinatorics.SetFamily.KruskalKatona` `Mathlib.Combinatorics.SetFamily.LYM` `Mathlib.Combinatorics.SetFamily.Shadow` `Mathlib.Combinatorics.SimpleGraph.Density` `Mathlib.Combinatorics.SimpleGraph.Extremal.Basic` `Mathlib.Combinatorics.SimpleGraph.IncMatrix` `Mathlib.Combinatorics.SimpleGraph.Init` `Mathlib.Combinatorics.SimpleGraph.Regularity.Energy` `Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform` `Mathlib.Computability.Ackermann` `Mathlib.Computability.DFA` `Mathlib.Computability.Encoding` `Mathlib.Computability.EpsilonNFA` `Mathlib.Computability.MyhillNerode` `Mathlib.Computability.NFA` `Mathlib.Computability.TMComputable` `Mathlib.Computability.TMToPartrec` `Mathlib.Control.Applicative` `Mathlib.Control.Basic` `Mathlib.Control.Combinators` `Mathlib.Control.EquivFunctor` `Mathlib.Control.Functor` `Mathlib.Control.Lawful` `Mathlib.Control.Monad.Basic` `Mathlib.Control.Monad.Cont` `Mathlib.Control.Monad.Writer` `Mathlib.Control.Traversable.Basic` `Mathlib.Control.Traversable.Equiv` `Mathlib.Control.Traversable.Lemmas` `Mathlib.Control.ULift` `Mathlib.Data.Array.Defs` `Mathlib.Data.Array.Extract` `Mathlib.Data.Bool.AllAny` `Mathlib.Data.Bool.Basic` `Mathlib.Data.Bool.Set` `Mathlib.Data.Bracket` `Mathlib.Data.Bundle` `Mathlib.Data.Char` `Mathlib.Data.Complex.Basic` `Mathlib.Data.Complex.BigOperators` `Mathlib.Data.Complex.Module` `Mathlib.Data.Countable.Defs` `Mathlib.Data.Countable.Small` `Mathlib.Data.DFinsupp.BigOperators` `Mathlib.Data.DFinsupp.Interval` `Mathlib.Data.DFinsupp.Lex` `Mathlib.Data.DFinsupp.Module` `Mathlib.Data.DFinsupp.Multiset` `Mathlib.Data.DFinsupp.Order` `Mathlib.Data.DFinsupp.Sigma` `Mathlib.Data.DFinsupp.Small` `Mathlib.Data.DFinsupp.Submonoid` `Mathlib.Data.DFinsupp.WellFounded` `Mathlib.Data.ENNReal.Action` `Mathlib.Data.ENNReal.Basic` `Mathlib.Data.ENNReal.BigOperators` `Mathlib.Data.ENNReal.Holder` `Mathlib.Data.ENNReal.Inv` `Mathlib.Data.ENNReal.Lemmas` `Mathlib.Data.ENNReal.Operations` `Mathlib.Data.ENNReal.Order` `Mathlib.Data.ENNReal.Real` `Mathlib.Data.ENat.Defs` `Mathlib.Data.EReal.Basic` `Mathlib.Data.EReal.Inv` `Mathlib.Data.EReal.Operations` `Mathlib.Data.Erased` `Mathlib.Data.Fin.Tuple.NatAntidiagonal` `Mathlib.Data.Fin.Tuple.Reflection` `Mathlib.Data.Finite.Defs` `Mathlib.Data.Finset.Attr` `Mathlib.Data.Finset.Density` `Mathlib.Data.Finset.Finsupp` `Mathlib.Data.Finset.Grade` `Mathlib.Data.Finset.Interval` `Mathlib.Data.Finset.NatDivisors` `Mathlib.Data.Finsupp.AList` `Mathlib.Data.Finsupp.Antidiagonal` `Mathlib.Data.Finsupp.Basic` `Mathlib.Data.Finsupp.Encodable` `Mathlib.Data.Finsupp.Interval` `Mathlib.Data.Finsupp.Lex` `Mathlib.Data.Finsupp.MonomialOrder.DegLex` `Mathlib.Data.Finsupp.MonomialOrder` `Mathlib.Data.Finsupp.Multiset` `Mathlib.Data.Finsupp.Order` `Mathlib.Data.Finsupp.PWO` `Mathlib.Data.Finsupp.SMul` `Mathlib.Data.Finsupp.ToDFinsupp` `Mathlib.Data.Finsupp.Weight` `Mathlib.Data.Finsupp.WellFounded` `Mathlib.Data.FunLike.Basic` `Mathlib.Data.FunLike.Embedding` `Mathlib.Data.FunLike.Equiv` `Mathlib.Data.Ineq` `Mathlib.Data.Int.AbsoluteValue` `Mathlib.Data.Int.Associated` `Mathlib.Data.Int.Basic` `Mathlib.Data.Int.Bitwise` `Mathlib.Data.Int.CardIntervalMod` `Mathlib.Data.Int.Cast.Basic` `Mathlib.Data.Int.Cast.Defs` `Mathlib.Data.Int.Cast.Lemmas` `Mathlib.Data.Int.Cast.Pi` `Mathlib.Data.Int.Cast.Prod` `Mathlib.Data.Int.CharZero` `Mathlib.Data.Int.DivMod` `Mathlib.Data.Int.Init` `Mathlib.Data.Int.Interval` `Mathlib.Data.Int.Lemmas` `Mathlib.Data.Int.Log` `Mathlib.Data.Int.Notation` `Mathlib.Data.Int.Order.Basic` `Mathlib.Data.Int.Order.Lemmas` `Mathlib.Data.Int.Order.Units` `Mathlib.Data.Int.Range` `Mathlib.Data.Int.Star` `Mathlib.Data.Int.SuccPred` `Mathlib.Data.Int.WithZero` `Mathlib.Data.List.Defs` `Mathlib.Data.List.EditDistance.Defs` `Mathlib.Data.List.Flatten` `Mathlib.Data.List.GetD` `Mathlib.Data.List.Iterate` `Mathlib.Data.List.Lookmap` `Mathlib.Data.List.ModifyLast` `Mathlib.Data.List.Monad` `Mathlib.Data.List.Pairwise` `Mathlib.Data.List.Scan` `Mathlib.Data.List.Shortlex` `Mathlib.Data.List.SplitLengths` `Mathlib.Data.List.TFAE` `Mathlib.Data.List.TakeWhile` `Mathlib.Data.List.Triplewise` `Mathlib.Data.Matrix.Auto` `Mathlib.Data.Matrix.Basic` `Mathlib.Data.Matrix.Basis` `Mathlib.Data.Matrix.Bilinear` `Mathlib.Data.Matrix.Block` `Mathlib.Data.Matrix.ColumnRowPartitioned` `Mathlib.Data.Matrix.Composition` `Mathlib.Data.Matrix.ConjTranspose` `Mathlib.Data.Matrix.DMatrix` `Mathlib.Data.Matrix.DualNumber` `Mathlib.Data.Matrix.Hadamard` `Mathlib.Data.Matrix.Invertible` `Mathlib.Data.Matrix.Mul` `Mathlib.Data.Matrix.Notation` `Mathlib.Data.Matrix.PEquiv` `Mathlib.Data.Matrix.Reflection` `Mathlib.Data.Matrix.RowCol` `Mathlib.Data.Matroid.Init` `Mathlib.Data.Multiset.Interval` `Mathlib.Data.NNRat.BigOperators` `Mathlib.Data.NNRat.Defs` `Mathlib.Data.NNRat.Floor` `Mathlib.Data.NNRat.Lemmas` `Mathlib.Data.NNRat.Order` `Mathlib.Data.NNReal.Basic` `Mathlib.Data.NNReal.Defs` `Mathlib.Data.NNReal.Star` `Mathlib.Data.Nat.Basic` `Mathlib.Data.Nat.BinaryRec` `Mathlib.Data.Nat.Bits` `Mathlib.Data.Nat.Cast.Commute` `Mathlib.Data.Nat.Cast.Defs` `Mathlib.Data.Nat.Cast.NeZero` `Mathlib.Data.Nat.Cast.Order.Field` `Mathlib.Data.Nat.Cast.Prod` `Mathlib.Data.Nat.Cast.SetInterval` `Mathlib.Data.Nat.Cast.Synonym` `Mathlib.Data.Nat.Cast.WithTop` `Mathlib.Data.Nat.Choose.Cast` `Mathlib.Data.Nat.Choose.Central` `Mathlib.Data.Nat.Choose.Factorization` `Mathlib.Data.Nat.Choose.Mul` `Mathlib.Data.Nat.Choose.Multinomial` `Mathlib.Data.Nat.Choose.Sum` `Mathlib.Data.Nat.Choose.Vandermonde` `Mathlib.Data.Nat.Digits.Defs` `Mathlib.Data.Nat.Digits.Div` `Mathlib.Data.Nat.Digits.Lemmas` `Mathlib.Data.Nat.Factorial.BigOperators` `Mathlib.Data.Nat.Factorial.Cast` `Mathlib.Data.Nat.Factorial.DoubleFactorial` `Mathlib.Data.Nat.Factorial.NatCast` `Mathlib.Data.Nat.Factorization.Basic` `Mathlib.Data.Nat.Factorization.Defs` `Mathlib.Data.Nat.Factorization.Induction` `Mathlib.Data.Nat.Factorization.PrimePow` `Mathlib.Data.Nat.Factorization.Root` `Mathlib.Data.Nat.Fib.Basic` `Mathlib.Data.Nat.Fib.Zeckendorf` `Mathlib.Data.Nat.Find` `Mathlib.Data.Nat.Hyperoperation` `Mathlib.Data.Nat.Init` `Mathlib.Data.Nat.Log` `Mathlib.Data.Nat.Multiplicity` `Mathlib.Data.Nat.Notation` `Mathlib.Data.Nat.Order.Lemmas` `Mathlib.Data.Nat.PSub` `Mathlib.Data.Nat.Pairing` `Mathlib.Data.Nat.PartENat` `Mathlib.Data.Nat.Prime.Int` `Mathlib.Data.Nat.Set` `Mathlib.Data.Nat.Size` `Mathlib.Data.Nat.Sqrt` `Mathlib.Data.Nat.Squarefree` `Mathlib.Data.Nat.Upto` `Mathlib.Data.Num.Basic` `Mathlib.Data.Num.Lemmas` `Mathlib.Data.Num.Prime` `Mathlib.Data.Num.ZNum` `Mathlib.Data.Opposite` `Mathlib.Data.Option.Basic` `Mathlib.Data.Option.Defs` `Mathlib.Data.Option.NAry` `Mathlib.Data.Ordering.Basic` `Mathlib.Data.Ordering.Lemmas` `Mathlib.Data.Ordmap.Invariants` `Mathlib.Data.Ordmap.Ordnode` `Mathlib.Data.Ordmap.Ordset` `Mathlib.Data.PEquiv` `Mathlib.Data.PFun` `Mathlib.Data.PNat.Defs` `Mathlib.Data.PNat.Equiv` `Mathlib.Data.PNat.Notation` `Mathlib.Data.PNat.Xgcd` `Mathlib.Data.PSigma.Order` `Mathlib.Data.Part` `Mathlib.Data.Prod.Basic` `Mathlib.Data.Prod.Lex` `Mathlib.Data.Prod.PProd` `Mathlib.Data.Quot` `Mathlib.Data.Rat.BigOperators` `Mathlib.Data.Rat.Cardinal` `Mathlib.Data.Rat.Cast.CharZero` `Mathlib.Data.Rat.Cast.Defs` `Mathlib.Data.Rat.Cast.Lemmas` `Mathlib.Data.Rat.Cast.Order` `Mathlib.Data.Rat.Denumerable` `Mathlib.Data.Rat.Floor` `Mathlib.Data.Rat.Init` `Mathlib.Data.Rat.Lemmas` `Mathlib.Data.Rat.Sqrt` `Mathlib.Data.Rat.Star` `Mathlib.Data.Real.Archimedean` `Mathlib.Data.Real.Basic` `Mathlib.Data.Real.ConjExponents` `Mathlib.Data.Real.ENatENNReal` `Mathlib.Data.Real.EReal` `Mathlib.Data.Real.Pointwise` `Mathlib.Data.Real.Sign` `Mathlib.Data.Real.Star` `Mathlib.Data.Rel` `Mathlib.Data.SProd` `Mathlib.Data.Semiquot` `Mathlib.Data.Set.Accumulate` `Mathlib.Data.Set.Basic` `Mathlib.Data.Set.BoolIndicator` `Mathlib.Data.Set.BooleanAlgebra` `Mathlib.Data.Set.CoeSort` `Mathlib.Data.Set.Defs` `Mathlib.Data.Set.Disjoint` `Mathlib.Data.Set.Function` `Mathlib.Data.Set.Functor` `Mathlib.Data.Set.Image` `Mathlib.Data.Set.Inclusion` `Mathlib.Data.Set.Insert` `Mathlib.Data.Set.Lattice.Image` `Mathlib.Data.Set.Lattice` `Mathlib.Data.Set.List` `Mathlib.Data.Set.Monotone` `Mathlib.Data.Set.NAry` `Mathlib.Data.Set.Notation` `Mathlib.Data.Set.Operations` `Mathlib.Data.Set.Opposite` `Mathlib.Data.Set.Order` `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.Subsingleton` `Mathlib.Data.Set.SymmDiff` `Mathlib.Data.Set.UnionLift` `Mathlib.Data.SetLike.Basic` `Mathlib.Data.Setoid.Basic` `Mathlib.Data.Sigma.Basic` `Mathlib.Data.Sigma.Lex` `Mathlib.Data.Sigma.Order` `Mathlib.Data.Sign` `Mathlib.Data.Stream.Defs` `Mathlib.Data.String.Defs` `Mathlib.Data.String.Lemmas` `Mathlib.Data.Subtype` `Mathlib.Data.Sum.Basic` `Mathlib.Data.Sum.Lattice` `Mathlib.Data.Sum.Order` `Mathlib.Data.Sym.Sym2.Init` `Mathlib.Data.Tree.Basic` `Mathlib.Data.Tree.Get` `Mathlib.Data.Tree.RBMap` `Mathlib.Data.Tree.Traversable` `Mathlib.Data.TwoPointing` `Mathlib.Data.UInt` `Mathlib.Data.ULift` `Mathlib.Deprecated.Aliases` `Mathlib.Deprecated.Cardinal.Continuum` `Mathlib.Deprecated.Cardinal.PartENat` `Mathlib.Deprecated.Order` `Mathlib.Dynamics.BirkhoffSum.Average` `Mathlib.Dynamics.Flow` `Mathlib.Dynamics.Minimal` `Mathlib.Dynamics.OmegaLimit` `Mathlib.FieldTheory.IntermediateField.Adjoin.Defs` `Mathlib.FieldTheory.IntermediateField.Basic` `Mathlib.FieldTheory.RatFunc.Basic` `Mathlib.FieldTheory.RatFunc.Defs` `Mathlib.Geometry.Convex.Cone.Basic` `Mathlib.Geometry.Convex.Cone.Pointed` `Mathlib.Geometry.Manifold.ChartedSpace` `Mathlib.Geometry.Manifold.LocalInvariantProperties` `Mathlib.Geometry.Manifold.Sheaf.Basic` `Mathlib.Geometry.RingedSpace.Basic` `Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits` `Mathlib.Geometry.RingedSpace.SheafedSpace` `Mathlib.Geometry.RingedSpace.Stalks` `Mathlib.GroupTheory.ArchimedeanDensely` `Mathlib.GroupTheory.Archimedean` `Mathlib.GroupTheory.Congruence.Basic` `Mathlib.GroupTheory.Congruence.Defs` `Mathlib.GroupTheory.Congruence.Hom` `Mathlib.GroupTheory.Congruence.Opposite` `Mathlib.GroupTheory.Coxeter.Basic` `Mathlib.GroupTheory.Coxeter.Matrix` `Mathlib.GroupTheory.Divisible` `Mathlib.GroupTheory.EckmannHilton` `Mathlib.GroupTheory.GroupAction.DomAct.ActionHom` `Mathlib.GroupTheory.GroupAction.DomAct.Basic` `Mathlib.GroupTheory.GroupAction.Embedding` `Mathlib.GroupTheory.GroupAction.Hom` `Mathlib.GroupTheory.GroupAction.IterateAct` `Mathlib.GroupTheory.GroupAction.Pointwise` `Mathlib.GroupTheory.GroupAction.Quotient` `Mathlib.GroupTheory.GroupAction.Ring` `Mathlib.GroupTheory.GroupAction.Support` `Mathlib.GroupTheory.OreLocalization.OreSet` `Mathlib.GroupTheory.Perm.Option` `Mathlib.GroupTheory.Perm.Sign` `Mathlib.GroupTheory.QuotientGroup.Basic` `Mathlib.GroupTheory.Submonoid.Center` `Mathlib.GroupTheory.Submonoid.Centralizer` `Mathlib.GroupTheory.Subsemigroup.Center` `Mathlib.GroupTheory.Subsemigroup.Centralizer` `Mathlib.InformationTheory.Hamming` `Mathlib.Init` `Mathlib.Lean.CoreM` `Mathlib.Lean.Elab.Tactic.Basic` `Mathlib.Lean.Elab.Term` `Mathlib.Lean.EnvExtension` `Mathlib.Lean.Exception` `Mathlib.Lean.Expr.Basic` `Mathlib.Lean.Expr.ExtraRecognizers` `Mathlib.Lean.Expr.Rat` `Mathlib.Lean.Expr.ReplaceRec` `Mathlib.Lean.Expr` `Mathlib.Lean.GoalsLocation` `Mathlib.Lean.Json` `Mathlib.Lean.LocalContext` `Mathlib.Lean.Message` `Mathlib.Lean.Meta.Basic` `Mathlib.Lean.Meta.CongrTheorems` `Mathlib.Lean.Meta.DiscrTree` `Mathlib.Lean.Meta.KAbstractPositions` `Mathlib.Lean.Meta.RefinedDiscrTree.Basic` `Mathlib.Lean.Meta.RefinedDiscrTree.Encode` `Mathlib.Lean.Meta.RefinedDiscrTree.Initialize` `Mathlib.Lean.Meta.RefinedDiscrTree.Lookup` `Mathlib.Lean.Meta.RefinedDiscrTree` `Mathlib.Lean.Meta.Simp` `Mathlib.Lean.Meta` `Mathlib.Lean.Name` `Mathlib.Lean.PrettyPrinter.Delaborator` `Mathlib.Lean.Thunk` `Mathlib.LinearAlgebra.AffineSpace.AffineEquiv` `Mathlib.LinearAlgebra.AffineSpace.AffineMap` `Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic` `Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs` `Mathlib.LinearAlgebra.AffineSpace.Combination` `Mathlib.LinearAlgebra.AffineSpace.Defs` `Mathlib.LinearAlgebra.AffineSpace.MidpointZero` `Mathlib.LinearAlgebra.AffineSpace.Midpoint` `Mathlib.LinearAlgebra.AffineSpace.Ordered` `Mathlib.LinearAlgebra.AffineSpace.Pointwise` `Mathlib.LinearAlgebra.AffineSpace.Restrict` `Mathlib.LinearAlgebra.AffineSpace.Slope` `Mathlib.LinearAlgebra.Alternating.Basic` `Mathlib.LinearAlgebra.Alternating.Curry` `Mathlib.LinearAlgebra.Basis.Basic` `Mathlib.LinearAlgebra.Basis.Bilinear` `Mathlib.LinearAlgebra.Basis.Cardinality` `Mathlib.LinearAlgebra.Basis.Defs` `Mathlib.LinearAlgebra.Basis.Fin` `Mathlib.LinearAlgebra.Basis.Flag` `Mathlib.LinearAlgebra.Basis.Prod` `Mathlib.LinearAlgebra.Basis.SMul` `Mathlib.LinearAlgebra.Basis.Submodule` `Mathlib.LinearAlgebra.BilinearForm.Basic` `Mathlib.LinearAlgebra.BilinearForm.Hom` `Mathlib.LinearAlgebra.BilinearMap` `Mathlib.LinearAlgebra.Countable` `Mathlib.LinearAlgebra.DFinsupp` `Mathlib.LinearAlgebra.DirectSum.Basis` `Mathlib.LinearAlgebra.DirectSum.Finsupp` `Mathlib.LinearAlgebra.DirectSum.TensorProduct` `Mathlib.LinearAlgebra.Dual.Basis` `Mathlib.LinearAlgebra.Dual.Defs` `Mathlib.LinearAlgebra.Finsupp.Defs` `Mathlib.LinearAlgebra.Finsupp.LSum` `Mathlib.LinearAlgebra.Finsupp.LinearCombination` `Mathlib.LinearAlgebra.Finsupp.Pi` `Mathlib.LinearAlgebra.Finsupp.Span` `Mathlib.LinearAlgebra.Finsupp.SumProd` `Mathlib.LinearAlgebra.Finsupp.Supported` `Mathlib.LinearAlgebra.Finsupp.VectorSpace` `Mathlib.LinearAlgebra.FreeModule.Basic` `Mathlib.LinearAlgebra.FreeProduct.Basic` `Mathlib.LinearAlgebra.GeneralLinearGroup` `Mathlib.LinearAlgebra.LinearIndependent.Basic` `Mathlib.LinearAlgebra.LinearIndependent.Defs` `Mathlib.LinearAlgebra.LinearIndependent.Lemmas` `Mathlib.LinearAlgebra.LinearPMap` `Mathlib.LinearAlgebra.Matrix.Circulant` `Mathlib.LinearAlgebra.Matrix.DotProduct` `Mathlib.LinearAlgebra.Matrix.Dual` `Mathlib.LinearAlgebra.Matrix.Integer` `Mathlib.LinearAlgebra.Matrix.Orthogonal` `Mathlib.LinearAlgebra.Matrix.Permanent` `Mathlib.LinearAlgebra.Matrix.SemiringInverse` `Mathlib.LinearAlgebra.Matrix.StdBasis` `Mathlib.LinearAlgebra.Matrix.Symmetric` `Mathlib.LinearAlgebra.Matrix.ToLin` `Mathlib.LinearAlgebra.Matrix.Trace` `Mathlib.LinearAlgebra.Matrix.Unique` `Mathlib.LinearAlgebra.Multilinear.Basic` `Mathlib.LinearAlgebra.Multilinear.Basis` `Mathlib.LinearAlgebra.Multilinear.Curry` `Mathlib.LinearAlgebra.Multilinear.DFinsupp` `Mathlib.LinearAlgebra.Multilinear.Pi` `Mathlib.LinearAlgebra.Multilinear.TensorProduct` `Mathlib.LinearAlgebra.PiTensorProduct` `Mathlib.LinearAlgebra.Pi` `Mathlib.LinearAlgebra.Prod` `Mathlib.LinearAlgebra.Quotient.Defs` `Mathlib.LinearAlgebra.Ray` `Mathlib.LinearAlgebra.SModEq` `Mathlib.LinearAlgebra.SesquilinearForm` `Mathlib.LinearAlgebra.Span.Basic` `Mathlib.LinearAlgebra.Span.Defs` `Mathlib.LinearAlgebra.StdBasis` `Mathlib.LinearAlgebra.SymmetricAlgebra.Basic` `Mathlib.LinearAlgebra.TensorAlgebra.Basic` `Mathlib.LinearAlgebra.TensorAlgebra.Grading` `Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower` `Mathlib.LinearAlgebra.TensorPower.Basic` `Mathlib.LinearAlgebra.TensorPower.Pairing` `Mathlib.LinearAlgebra.TensorProduct.Associator` `Mathlib.LinearAlgebra.TensorProduct.Basic` `Mathlib.LinearAlgebra.TensorProduct.Basis` `Mathlib.LinearAlgebra.TensorProduct.DirectLimit` `Mathlib.LinearAlgebra.TensorProduct.Finiteness` `Mathlib.LinearAlgebra.TensorProduct.Opposite` `Mathlib.LinearAlgebra.TensorProduct.Pi` `Mathlib.LinearAlgebra.TensorProduct.Prod` `Mathlib.LinearAlgebra.TensorProduct.Subalgebra` `Mathlib.LinearAlgebra.TensorProduct.Submodule` `Mathlib.LinearAlgebra.TensorProduct.Tower` `Mathlib.Logic.Basic` `Mathlib.Logic.Embedding.Basic` `Mathlib.Logic.Embedding.Set` `Mathlib.Logic.Equiv.Basic` `Mathlib.Logic.Equiv.Defs` `Mathlib.Logic.Equiv.Embedding` `Mathlib.Logic.Equiv.Nat` `Mathlib.Logic.Equiv.Option` `Mathlib.Logic.Equiv.Pairwise` `Mathlib.Logic.Equiv.PartialEquiv` `Mathlib.Logic.Equiv.Prod` `Mathlib.Logic.Equiv.Set` `Mathlib.Logic.Equiv.Sum` `Mathlib.Logic.ExistsUnique` `Mathlib.Logic.Function.Basic` `Mathlib.Logic.Function.Coequalizer` `Mathlib.Logic.Function.CompTypeclasses` `Mathlib.Logic.Function.Conjugate` `Mathlib.Logic.Function.Defs` `Mathlib.Logic.Function.DependsOn` `Mathlib.Logic.Function.FiberPartition` `Mathlib.Logic.Function.Iterate` `Mathlib.Logic.Function.ULift` `Mathlib.Logic.Hydra` `Mathlib.Logic.IsEmpty` `Mathlib.Logic.Lemmas` `Mathlib.Logic.Nonempty` `Mathlib.Logic.Nontrivial.Basic` `Mathlib.Logic.Nontrivial.Defs` `Mathlib.Logic.OpClass` `Mathlib.Logic.Pairwise` `Mathlib.Logic.Relation` `Mathlib.Logic.Relator` `Mathlib.Logic.Small.Basic` `Mathlib.Logic.Small.Defs` `Mathlib.Logic.Small.Set` `Mathlib.Logic.Unique` `Mathlib.Logic.UnivLE` `Mathlib.MeasureTheory.Constructions.AddChar` `Mathlib.MeasureTheory.OuterMeasure.Defs` `Mathlib.ModelTheory.Bundled` `Mathlib.ModelTheory.Complexity` `Mathlib.ModelTheory.DirectLimit` `Mathlib.ModelTheory.ElementaryMaps` `Mathlib.ModelTheory.ElementarySubstructures` `Mathlib.ModelTheory.Encoding` `Mathlib.ModelTheory.Equivalence` `Mathlib.ModelTheory.FinitelyGenerated` `Mathlib.ModelTheory.Fraisse` `Mathlib.ModelTheory.Graph` `Mathlib.ModelTheory.Order` `Mathlib.ModelTheory.PartialEquiv` `Mathlib.ModelTheory.Satisfiability` `Mathlib.ModelTheory.Skolem` `Mathlib.ModelTheory.Substructures` `Mathlib.ModelTheory.Types` `Mathlib.NumberTheory.ADEInequality` `Mathlib.NumberTheory.ArithmeticFunction` `Mathlib.NumberTheory.Basic` `Mathlib.NumberTheory.ClassNumber.AdmissibleAbs` `Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue` `Mathlib.NumberTheory.Dioph` `Mathlib.NumberTheory.Divisors` `Mathlib.NumberTheory.EllipticDivisibilitySequence` `Mathlib.NumberTheory.FLT.Basic` `Mathlib.NumberTheory.FLT.MasonStothers` `Mathlib.NumberTheory.FactorisationProperties` `Mathlib.NumberTheory.FrobeniusNumber` `Mathlib.NumberTheory.MaricaSchoenheim` `Mathlib.NumberTheory.Multiplicity` `Mathlib.NumberTheory.Padics.PadicNorm` `Mathlib.NumberTheory.Padics.PadicVal.Basic` `Mathlib.NumberTheory.Padics.PadicVal.Defs` `Mathlib.NumberTheory.PellMatiyasevic` `Mathlib.NumberTheory.Primorial` `Mathlib.NumberTheory.SelbergSieve` `Mathlib.NumberTheory.SmoothNumbers` `Mathlib.NumberTheory.Zsqrtd.Basic` `Mathlib.NumberTheory.Zsqrtd.GaussianInt` `Mathlib.Order.Antichain` `Mathlib.Order.Antisymmetrization` `Mathlib.Order.Basic` `Mathlib.Order.BooleanAlgebra` `Mathlib.Order.Booleanisation` `Mathlib.Order.BoundedOrder.Basic` `Mathlib.Order.BoundedOrder.Lattice` `Mathlib.Order.BoundedOrder.Monotone` `Mathlib.Order.Bounded` `Mathlib.Order.Bounds.Basic` `Mathlib.Order.Bounds.Defs` `Mathlib.Order.Bounds.Image` `Mathlib.Order.Bounds.Lattice` `Mathlib.Order.Bounds.OrderIso` `Mathlib.Order.Chain` `Mathlib.Order.Circular` `Mathlib.Order.Closure` `Mathlib.Order.Cofinal` `Mathlib.Order.Comparable` `Mathlib.Order.Compare` `Mathlib.Order.CompleteBooleanAlgebra` `Mathlib.Order.CompleteLattice.Basic` `Mathlib.Order.CompleteLattice.Chain` `Mathlib.Order.CompleteLattice.Defs` `Mathlib.Order.CompleteLattice.Group` `Mathlib.Order.CompleteLattice.Lemmas` `Mathlib.Order.Concept` `Mathlib.Order.ConditionallyCompleteLattice.Basic` `Mathlib.Order.ConditionallyCompleteLattice.Defs` `Mathlib.Order.ConditionallyCompleteLattice.Group` `Mathlib.Order.ConditionallyCompleteLattice.Indexed` `Mathlib.Order.Copy` `Mathlib.Order.Defs.LinearOrder` `Mathlib.Order.Defs.PartialOrder` `Mathlib.Order.Defs.Unbundled` `Mathlib.Order.Directed` `Mathlib.Order.Disjoint` `Mathlib.Order.Estimator` `Mathlib.Order.Extension.Linear` `Mathlib.Order.Filter.AtTopBot.Archimedean` `Mathlib.Order.Filter.AtTopBot.Basic` `Mathlib.Order.Filter.AtTopBot.CompleteLattice` `Mathlib.Order.Filter.AtTopBot.Defs` `Mathlib.Order.Filter.AtTopBot.Disjoint` `Mathlib.Order.Filter.AtTopBot.Field` `Mathlib.Order.Filter.AtTopBot.Floor` `Mathlib.Order.Filter.AtTopBot.Group` `Mathlib.Order.Filter.AtTopBot.Map` `Mathlib.Order.Filter.AtTopBot.ModEq` `Mathlib.Order.Filter.AtTopBot.Monoid` `Mathlib.Order.Filter.AtTopBot.Ring` `Mathlib.Order.Filter.AtTopBot.Tendsto` `Mathlib.Order.Filter.Bases.Basic` `Mathlib.Order.Filter.Basic` `Mathlib.Order.Filter.CardinalInter` `Mathlib.Order.Filter.Cocardinal` `Mathlib.Order.Filter.Curry` `Mathlib.Order.Filter.Defs` `Mathlib.Order.Filter.ENNReal` `Mathlib.Order.Filter.Ker` `Mathlib.Order.Filter.Map` `Mathlib.Order.Filter.NAry` `Mathlib.Order.Filter.Partial` `Mathlib.Order.Filter.Prod` `Mathlib.Order.Filter.Tendsto` `Mathlib.Order.GaloisConnection.Basic` `Mathlib.Order.GaloisConnection.Defs` `Mathlib.Order.Grade` `Mathlib.Order.Heyting.Basic` `Mathlib.Order.Heyting.Hom` `Mathlib.Order.Heyting.Regular` `Mathlib.Order.Hom.Basic` `Mathlib.Order.Hom.BoundedLattice` `Mathlib.Order.Hom.Bounded` `Mathlib.Order.Hom.CompleteLattice` `Mathlib.Order.Hom.Lattice` `Mathlib.Order.Hom.Order` `Mathlib.Order.Hom.Set` `Mathlib.Order.Hom.WithTopBot` `Mathlib.Order.Interval.Basic` `Mathlib.Order.Interval.Finset.Box` `Mathlib.Order.Interval.Set.Basic` `Mathlib.Order.Interval.Set.Defs` `Mathlib.Order.Interval.Set.Disjoint` `Mathlib.Order.Interval.Set.Image` `Mathlib.Order.Interval.Set.IsoIoo` `Mathlib.Order.Interval.Set.LinearOrder` `Mathlib.Order.Interval.Set.OrdConnectedLinear` `Mathlib.Order.Interval.Set.OrderIso` `Mathlib.Order.Interval.Set.SurjOn` `Mathlib.Order.Interval.Set.WithBotTop` `Mathlib.Order.Iterate` `Mathlib.Order.KonigLemma` `Mathlib.Order.LatticeIntervals` `Mathlib.Order.Lattice` `Mathlib.Order.Max` `Mathlib.Order.MinMax` `Mathlib.Order.Minimal` `Mathlib.Order.Monotone.Basic` `Mathlib.Order.Monotone.Defs` `Mathlib.Order.Monotone.Extension` `Mathlib.Order.Monotone.Monovary` `Mathlib.Order.Monotone.Odd` `Mathlib.Order.Monotone.Union` `Mathlib.Order.Nat` `Mathlib.Order.Notation` `Mathlib.Order.Nucleus` `Mathlib.Order.OrdContinuous` `Mathlib.Order.Preorder.Chain` `Mathlib.Order.Prod.Lex.Hom` `Mathlib.Order.PropInstances` `Mathlib.Order.Rel.GaloisConnection` `Mathlib.Order.RelClasses` `Mathlib.Order.RelIso.Basic` `Mathlib.Order.RelIso.Set` `Mathlib.Order.ScottContinuity` `Mathlib.Order.SemiconjSup` `Mathlib.Order.SetIsMax` `Mathlib.Order.SetNotation` `Mathlib.Order.Set` `Mathlib.Order.SymmDiff` `Mathlib.Order.Synonym` `Mathlib.Order.TypeTags` `Mathlib.Order.ULift` `Mathlib.Order.UpperLower.Relative` `Mathlib.Order.WellFounded` `Mathlib.Order.WithBot` `Mathlib.Order.Zorn` `Mathlib.RingTheory.Adjoin.Basic` `Mathlib.RingTheory.Adjoin.Polynomial` `Mathlib.RingTheory.AlgebraTower` `Mathlib.RingTheory.Algebraic.Cardinality` `Mathlib.RingTheory.Algebraic.Defs` `Mathlib.RingTheory.Algebraic.LinearIndependent` `Mathlib.RingTheory.Algebraic.Pi` `Mathlib.RingTheory.AlgebraicIndependent.Defs` `Mathlib.RingTheory.Bezout` `Mathlib.RingTheory.Bialgebra.Basic` `Mathlib.RingTheory.Bialgebra.Equiv` `Mathlib.RingTheory.Bialgebra.Hom` `Mathlib.RingTheory.Bialgebra.MonoidAlgebra` `Mathlib.RingTheory.Bialgebra.TensorProduct` `Mathlib.RingTheory.ChainOfDivisors` `Mathlib.RingTheory.Coalgebra.Basic` `Mathlib.RingTheory.Coalgebra.Equiv` `Mathlib.RingTheory.Coalgebra.Hom` `Mathlib.RingTheory.Coalgebra.MonoidAlgebra` `Mathlib.RingTheory.Coalgebra.TensorProduct` `Mathlib.RingTheory.Congruence.Basic` `Mathlib.RingTheory.Congruence.Defs` `Mathlib.RingTheory.Congruence.Opposite` `Mathlib.RingTheory.Coprime.Basic` `Mathlib.RingTheory.Coprime.Ideal` `Mathlib.RingTheory.Coprime.Lemmas` `Mathlib.RingTheory.Derivation.Basic` `Mathlib.RingTheory.Derivation.DifferentialRing` `Mathlib.RingTheory.DividedPowers.Basic` `Mathlib.RingTheory.DividedPowers.DPMorphism` `Mathlib.RingTheory.EuclideanDomain` `Mathlib.RingTheory.FilteredAlgebra.Basic` `Mathlib.RingTheory.Finiteness.Basic` `Mathlib.RingTheory.Finiteness.Bilinear` `Mathlib.RingTheory.Finiteness.Defs` `Mathlib.RingTheory.Finiteness.Lattice` `Mathlib.RingTheory.Finiteness.Nakayama` `Mathlib.RingTheory.Finiteness.Nilpotent` `Mathlib.RingTheory.Finiteness.Prod` `Mathlib.RingTheory.Finiteness.Subalgebra` `Mathlib.RingTheory.GradedAlgebra.Basic` `Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal` `Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule` `Mathlib.RingTheory.GradedAlgebra.Radical` `Mathlib.RingTheory.HahnSeries.Addition` `Mathlib.RingTheory.HahnSeries.HEval` `Mathlib.RingTheory.HahnSeries.Lex` `Mathlib.RingTheory.HahnSeries.Multiplication` `Mathlib.RingTheory.HahnSeries.PowerSeries` `Mathlib.RingTheory.HahnSeries.Summable` `Mathlib.RingTheory.HahnSeries.Valuation` `Mathlib.RingTheory.HopfAlgebra.Basic` `Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra` `Mathlib.RingTheory.HopfAlgebra.TensorProduct` `Mathlib.RingTheory.Ideal.Basic` `Mathlib.RingTheory.Ideal.Basis` `Mathlib.RingTheory.Ideal.BigOperators` `Mathlib.RingTheory.Ideal.Colon` `Mathlib.RingTheory.Ideal.Defs` `Mathlib.RingTheory.Ideal.IdempotentFG` `Mathlib.RingTheory.Ideal.IsPrincipal` `Mathlib.RingTheory.Ideal.Lattice` `Mathlib.RingTheory.Ideal.Maps` `Mathlib.RingTheory.Ideal.Maximal` `Mathlib.RingTheory.Ideal.Nonunits` `Mathlib.RingTheory.Ideal.Operations` `Mathlib.RingTheory.Ideal.Pointwise` `Mathlib.RingTheory.Ideal.Prime` `Mathlib.RingTheory.Ideal.Prod` `Mathlib.RingTheory.Ideal.Quotient.Defs` `Mathlib.RingTheory.Ideal.Span` `Mathlib.RingTheory.Int.Basic` `Mathlib.RingTheory.IntegralClosure.Algebra.Defs` `Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs` `Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs` `Mathlib.RingTheory.Invariant.Defs` `Mathlib.RingTheory.IsTensorProduct` `Mathlib.RingTheory.LocalRing.Basic` `Mathlib.RingTheory.LocalRing.Defs` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs` `Mathlib.RingTheory.LocalRing.Subring` `Mathlib.RingTheory.Localization.Away.Basic` `Mathlib.RingTheory.Localization.BaseChange` `Mathlib.RingTheory.Localization.Basic` `Mathlib.RingTheory.Localization.Cardinality` `Mathlib.RingTheory.Localization.Defs` `Mathlib.RingTheory.Localization.FractionRing` `Mathlib.RingTheory.Localization.Integer` `Mathlib.RingTheory.Localization.Module` `Mathlib.RingTheory.Localization.NumDen` `Mathlib.RingTheory.Localization.Pi` `Mathlib.RingTheory.Multiplicity` `Mathlib.RingTheory.MvPolynomial.EulerIdentity` `Mathlib.RingTheory.MvPolynomial.Groebner` `Mathlib.RingTheory.MvPolynomial.Homogeneous` `Mathlib.RingTheory.MvPolynomial.Ideal` `Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex` `Mathlib.RingTheory.MvPolynomial.MonomialOrder` `Mathlib.RingTheory.MvPolynomial.Symmetric.Defs` `Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem` `Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities` `Mathlib.RingTheory.MvPolynomial.Tower` `Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous` `Mathlib.RingTheory.MvPowerSeries.Basic` `Mathlib.RingTheory.MvPowerSeries.Inverse` `Mathlib.RingTheory.MvPowerSeries.LexOrder` `Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors` `Mathlib.RingTheory.MvPowerSeries.Order` `Mathlib.RingTheory.MvPowerSeries.Trunc` `Mathlib.RingTheory.Nilpotent.Basic` `Mathlib.RingTheory.Nilpotent.Exp` `Mathlib.RingTheory.Noetherian.Defs` `Mathlib.RingTheory.Noetherian.Filter` `Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain` `Mathlib.RingTheory.NonUnitalSubring.Basic` `Mathlib.RingTheory.NonUnitalSubsemiring.Basic` `Mathlib.RingTheory.NonUnitalSubsemiring.Defs` `Mathlib.RingTheory.OreLocalization.Cardinality` `Mathlib.RingTheory.OreLocalization.OreSet` `Mathlib.RingTheory.OreLocalization.Ring` `Mathlib.RingTheory.PiTensorProduct` `Mathlib.RingTheory.Polynomial.Bernstein` `Mathlib.RingTheory.Polynomial.Content` `Mathlib.RingTheory.Polynomial.Eisenstein.Generalized` `Mathlib.RingTheory.Polynomial.GaussNorm` `Mathlib.RingTheory.Polynomial.Hermite.Basic` `Mathlib.RingTheory.Polynomial.HilbertPoly` `Mathlib.RingTheory.Polynomial.Ideal` `Mathlib.RingTheory.Polynomial.IntegralNormalization` `Mathlib.RingTheory.Polynomial.Opposites` `Mathlib.RingTheory.Polynomial.Pochhammer` `Mathlib.RingTheory.Polynomial.Radical` `Mathlib.RingTheory.Polynomial.ScaleRoots` `Mathlib.RingTheory.Polynomial.ShiftedLegendre` `Mathlib.RingTheory.Polynomial.SmallDegreeVieta` `Mathlib.RingTheory.Polynomial.Tower` `Mathlib.RingTheory.Polynomial.Vieta` `Mathlib.RingTheory.Polynomial.Wronskian` `Mathlib.RingTheory.PolynomialAlgebra` `Mathlib.RingTheory.PolynomialLaw.Basic` `Mathlib.RingTheory.PowerSeries.Basic` `Mathlib.RingTheory.PowerSeries.CoeffMulMem` `Mathlib.RingTheory.PowerSeries.GaussNorm` `Mathlib.RingTheory.PowerSeries.NoZeroDivisors` `Mathlib.RingTheory.PowerSeries.Order` `Mathlib.RingTheory.PowerSeries.Trunc` `Mathlib.RingTheory.PowerSeries.WellKnown` `Mathlib.RingTheory.PrincipalIdealDomainOfPrime` `Mathlib.RingTheory.PrincipalIdealDomain` `Mathlib.RingTheory.Radical` `Mathlib.RingTheory.RingInvo` `Mathlib.RingTheory.SimpleRing.Basic` `Mathlib.RingTheory.SimpleRing.Congr` `Mathlib.RingTheory.SimpleRing.Defs` `Mathlib.RingTheory.SimpleRing.Field` `Mathlib.RingTheory.Spectrum.Maximal.Basic` `Mathlib.RingTheory.Spectrum.Maximal.Defs` `Mathlib.RingTheory.Spectrum.Prime.Defs` `Mathlib.RingTheory.TensorProduct.Basic` `Mathlib.RingTheory.TensorProduct.Free` `Mathlib.RingTheory.TensorProduct.IsBaseChangePi` `Mathlib.RingTheory.TensorProduct.MvPolynomial` `Mathlib.RingTheory.TensorProduct.Pi` `Mathlib.RingTheory.TwoSidedIdeal.Basic` `Mathlib.RingTheory.TwoSidedIdeal.BigOperators` `Mathlib.RingTheory.TwoSidedIdeal.Instances` `Mathlib.RingTheory.TwoSidedIdeal.Kernel` `Mathlib.RingTheory.TwoSidedIdeal.Lattice` `Mathlib.RingTheory.TwoSidedIdeal.Operations` `Mathlib.RingTheory.UniqueFactorizationDomain.Basic` `Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet` `Mathlib.RingTheory.UniqueFactorizationDomain.Finite` `Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp` `Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid` `Mathlib.RingTheory.UniqueFactorizationDomain.Ideal` `Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative` `Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity` `Mathlib.RingTheory.UniqueFactorizationDomain.Nat` `Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors` `Mathlib.RingTheory.Valuation.Archimedean` `Mathlib.RingTheory.Valuation.Basic` `Mathlib.RingTheory.Valuation.Discrete.Basic` `Mathlib.RingTheory.Valuation.ExtendToLocalization` `Mathlib.RingTheory.Valuation.Extension` `Mathlib.RingTheory.Valuation.Integers` `Mathlib.RingTheory.Valuation.PrimeMultiplicity` `Mathlib.RingTheory.Valuation.RankOne` `Mathlib.RingTheory.Valuation.ValExtension` `Mathlib.RingTheory.Valuation.ValuationRing` `Mathlib.SetTheory.Cardinal.Defs` `Mathlib.SetTheory.Cardinal.Finsupp` `Mathlib.SetTheory.Cardinal.Subfield` `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.Ordinal.NaturalOps` `Mathlib.SetTheory.Ordinal.Notation` `Mathlib.SetTheory.Ordinal.Topology` `Mathlib.SetTheory.PGame.Basic` `Mathlib.SetTheory.Surreal.Basic` `Mathlib.SetTheory.Surreal.Dyadic` `Mathlib.SetTheory.Surreal.Multiplication` `Mathlib.SetTheory.ZFC.PSet` `Mathlib.Std.Data.HashMap` `Mathlib.Tactic.Abel` `Mathlib.Tactic.AdaptationNote` `Mathlib.Tactic.Algebraize` `Mathlib.Tactic.ApplyAt` `Mathlib.Tactic.ApplyCongr` `Mathlib.Tactic.ApplyFun` `Mathlib.Tactic.ApplyWith` `Mathlib.Tactic.ArithMult.Init` `Mathlib.Tactic.ArithMult` `Mathlib.Tactic.Attr.Core` `Mathlib.Tactic.Attr.Register` `Mathlib.Tactic.Basic` `Mathlib.Tactic.Bound.Attribute` `Mathlib.Tactic.Bound.Init` `Mathlib.Tactic.Bound` `Mathlib.Tactic.ByContra` `Mathlib.Tactic.CC.Addition` `Mathlib.Tactic.CC.Datatypes` `Mathlib.Tactic.CC.Lemmas` `Mathlib.Tactic.CC.MkProof` `Mathlib.Tactic.CC` `Mathlib.Tactic.CancelDenoms.Core` `Mathlib.Tactic.CancelDenoms` `Mathlib.Tactic.CasesM` `Mathlib.Tactic.Cases` `Mathlib.Tactic.CategoryTheory.Coherence.Datatypes` `Mathlib.Tactic.CategoryTheory.Coherence.Normalize` `Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence` `Mathlib.Tactic.Change` `Mathlib.Tactic.Check` `Mathlib.Tactic.Choose` `Mathlib.Tactic.Clean` `Mathlib.Tactic.ClearExcept` `Mathlib.Tactic.ClearExclamation` `Mathlib.Tactic.Clear_` `Mathlib.Tactic.Coe` `Mathlib.Tactic.ComputeDegree` `Mathlib.Tactic.CongrExclamation` `Mathlib.Tactic.CongrM` `Mathlib.Tactic.Constructor` `Mathlib.Tactic.Continuity.Init` `Mathlib.Tactic.Continuity` `Mathlib.Tactic.ContinuousFunctionalCalculus` `Mathlib.Tactic.Contrapose` `Mathlib.Tactic.Conv` `Mathlib.Tactic.Convert` `Mathlib.Tactic.Core` `Mathlib.Tactic.DefEqTransformations` `Mathlib.Tactic.DeprecateTo` `Mathlib.Tactic.DeriveCountable` `Mathlib.Tactic.DeriveTraversable` `Mathlib.Tactic.Eqns` `Mathlib.Tactic.ErwQuestion` `Mathlib.Tactic.Eval` `Mathlib.Tactic.ExistsI` `Mathlib.Tactic.Explode.Datatypes` `Mathlib.Tactic.Explode.Pretty` `Mathlib.Tactic.Explode` `Mathlib.Tactic.ExtendDoc` `Mathlib.Tactic.ExtractGoal` `Mathlib.Tactic.ExtractLets` `Mathlib.Tactic.FBinop` `Mathlib.Tactic.FailIfNoProgress` `Mathlib.Tactic.FastInstance` `Mathlib.Tactic.FieldSimp` `Mathlib.Tactic.FindSyntax` `Mathlib.Tactic.Find` `Mathlib.Tactic.Finiteness.Attr` `Mathlib.Tactic.Finiteness` `Mathlib.Tactic.FunProp.Attr` `Mathlib.Tactic.FunProp.Core` `Mathlib.Tactic.FunProp.Decl` `Mathlib.Tactic.FunProp.Elab` `Mathlib.Tactic.FunProp.FunctionData` `Mathlib.Tactic.FunProp.Mor` `Mathlib.Tactic.FunProp.Theorems` `Mathlib.Tactic.FunProp.ToBatteries` `Mathlib.Tactic.FunProp.Types` `Mathlib.Tactic.FunProp` `Mathlib.Tactic.GCongr.CoreAttrs` `Mathlib.Tactic.GCongr.Core` `Mathlib.Tactic.GCongr.ForwardAttr` `Mathlib.Tactic.GCongr` `Mathlib.Tactic.GRewrite.Core` `Mathlib.Tactic.GRewrite.Elab` `Mathlib.Tactic.GRewrite` `Mathlib.Tactic.GeneralizeProofs` `Mathlib.Tactic.Generalize` `Mathlib.Tactic.Group` `Mathlib.Tactic.GuardGoalNums` `Mathlib.Tactic.GuardHypNums` `Mathlib.Tactic.HaveI` `Mathlib.Tactic.Have` `Mathlib.Tactic.HigherOrder` `Mathlib.Tactic.ITauto` `Mathlib.Tactic.InferParam` `Mathlib.Tactic.Inhabit` `Mathlib.Tactic.IntervalCases` `Mathlib.Tactic.IrreducibleDef` `Mathlib.Tactic.Lemma` `Mathlib.Tactic.LiftLets` `Mathlib.Tactic.Lift` `Mathlib.Tactic.Linarith.Datatypes` `Mathlib.Tactic.Linarith.Frontend` `Mathlib.Tactic.Linarith.Oracle.FourierMotzkin` `Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes` `Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss` `Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector` `Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm` `Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm` `Mathlib.Tactic.Linarith.Parsing` `Mathlib.Tactic.Linarith.Preprocessing` `Mathlib.Tactic.Linarith.Verification` `Mathlib.Tactic.Linarith` `Mathlib.Tactic.LinearCombination'` `Mathlib.Tactic.LinearCombination.Lemmas` `Mathlib.Tactic.LinearCombination` `Mathlib.Tactic.Linter.DeprecatedModule` `Mathlib.Tactic.Linter.PPRoundtrip` `Mathlib.Tactic.Linter.Style` `Mathlib.Tactic.Linter.TextBased` `Mathlib.Tactic.Linter.UpstreamableDecl` `Mathlib.Tactic.Measurability.Init` `Mathlib.Tactic.Measurability` `Mathlib.Tactic.MkIffOfInductiveProp` `Mathlib.Tactic.Module` `Mathlib.Tactic.Monotonicity.Attr` `Mathlib.Tactic.Monotonicity.Basic` `Mathlib.Tactic.Monotonicity.Lemmas` `Mathlib.Tactic.Monotonicity` `Mathlib.Tactic.MoveAdd` `Mathlib.Tactic.NoncommRing` `Mathlib.Tactic.Nontriviality.Core` `Mathlib.Tactic.Nontriviality` `Mathlib.Tactic.NormNum.Basic` `Mathlib.Tactic.NormNum.BigOperators` `Mathlib.Tactic.NormNum.Core` `Mathlib.Tactic.NormNum.DivMod` `Mathlib.Tactic.NormNum.Eq` `Mathlib.Tactic.NormNum.GCD` `Mathlib.Tactic.NormNum.Ineq` `Mathlib.Tactic.NormNum.Inv` `Mathlib.Tactic.NormNum.IsCoprime` `Mathlib.Tactic.NormNum.NatFactorial` `Mathlib.Tactic.NormNum.NatFib` `Mathlib.Tactic.NormNum.NatLog` `Mathlib.Tactic.NormNum.NatSqrt` `Mathlib.Tactic.NormNum.OfScientific` `Mathlib.Tactic.NormNum.PowMod` `Mathlib.Tactic.NormNum.Pow` `Mathlib.Tactic.NormNum.Prime` `Mathlib.Tactic.NormNum.Result` `Mathlib.Tactic.NormNum` `Mathlib.Tactic.NthRewrite` `Mathlib.Tactic.Observe` `Mathlib.Tactic.OfNat` `Mathlib.Tactic.Order.CollectFacts` `Mathlib.Tactic.Order.Graph.Basic` `Mathlib.Tactic.Order.Graph.Tarjan` `Mathlib.Tactic.Order.Preprocessing` `Mathlib.Tactic.Order` `Mathlib.Tactic.PPWithUniv` `Mathlib.Tactic.Peel` `Mathlib.Tactic.Polyrith` `Mathlib.Tactic.Positivity.Basic` `Mathlib.Tactic.Positivity.Core` `Mathlib.Tactic.Positivity.Finset` `Mathlib.Tactic.Positivity` `Mathlib.Tactic.ProdAssoc` `Mathlib.Tactic.Propose` `Mathlib.Tactic.ProxyType` `Mathlib.Tactic.Push` `Mathlib.Tactic.Qify` `Mathlib.Tactic.RSuffices` `Mathlib.Tactic.Recall` `Mathlib.Tactic.Recover` `Mathlib.Tactic.ReduceModChar.Ext` `Mathlib.Tactic.Relation.Rfl` `Mathlib.Tactic.Relation.Symm` `Mathlib.Tactic.RenameBVar` `Mathlib.Tactic.Rename` `Mathlib.Tactic.Replace` `Mathlib.Tactic.Rify` `Mathlib.Tactic.Ring.Basic` `Mathlib.Tactic.Ring.Compare` `Mathlib.Tactic.Ring.PNat` `Mathlib.Tactic.Ring.RingNF` `Mathlib.Tactic.Ring` `Mathlib.Tactic.Sat.FromLRAT` `Mathlib.Tactic.Says` `Mathlib.Tactic.ScopedNS` `Mathlib.Tactic.SetLike` `Mathlib.Tactic.Set` `Mathlib.Tactic.SimpIntro` `Mathlib.Tactic.SimpRw` `Mathlib.Tactic.Simproc.ExistsAndEq` `Mathlib.Tactic.Simproc.Factors` `Mathlib.Tactic.Simps.Basic` `Mathlib.Tactic.Simps.NotationClass` `Mathlib.Tactic.SplitIfs` `Mathlib.Tactic.Spread` `Mathlib.Tactic.StacksAttribute` `Mathlib.Tactic.Subsingleton` `Mathlib.Tactic.Substs` `Mathlib.Tactic.SuccessIfFailWithMsg` `Mathlib.Tactic.SudoSetOption` `Mathlib.Tactic.SuppressCompilation` `Mathlib.Tactic.SwapVar` `Mathlib.Tactic.TFAE` `Mathlib.Tactic.TautoSet` `Mathlib.Tactic.Tauto` `Mathlib.Tactic.TermCongr` `Mathlib.Tactic.ToAdditive.Frontend` `Mathlib.Tactic.ToAdditive` `Mathlib.Tactic.ToExpr` `Mathlib.Tactic.ToLevel` `Mathlib.Tactic.Trace` `Mathlib.Tactic.TryThis` `Mathlib.Tactic.TypeCheck` `Mathlib.Tactic.TypeStar` `Mathlib.Tactic.UnsetOption` `Mathlib.Tactic.Use` `Mathlib.Tactic.Variable` `Mathlib.Tactic.WLOG` `Mathlib.Tactic.Widget.Calc` `Mathlib.Tactic.Widget.CongrM` `Mathlib.Tactic.Widget.Conv` `Mathlib.Tactic.Widget.GCongr` `Mathlib.Tactic.Widget.InteractiveUnfold` `Mathlib.Tactic.Widget.SelectInsertParamsClass` `Mathlib.Tactic.Widget.SelectPanelUtils` `Mathlib.Tactic.WithoutCDot` `Mathlib.Tactic.Zify` `Mathlib.Testing.Plausible.Functions` `Mathlib.Testing.Plausible.Sampleable` `Mathlib.Testing.Plausible.Testable` `Mathlib.Topology.Algebra.Affine` `Mathlib.Topology.Algebra.Algebra.Rat` `Mathlib.Topology.Algebra.ConstMulAction` `Mathlib.Topology.Algebra.Equicontinuity` `Mathlib.Topology.Algebra.Field` `Mathlib.Topology.Algebra.FilterBasis` `Mathlib.Topology.Algebra.Group.Basic` `Mathlib.Topology.Algebra.Group.Compact` `Mathlib.Topology.Algebra.Group.GroupTopology` `Mathlib.Topology.Algebra.Group.OpenMapping` `Mathlib.Topology.Algebra.Group.Pointwise` `Mathlib.Topology.Algebra.Group.Quotient` `Mathlib.Topology.Algebra.Group.SubmonoidClosure` `Mathlib.Topology.Algebra.GroupCompletion` `Mathlib.Topology.Algebra.GroupWithZero` `Mathlib.Topology.Algebra.InfiniteSum.Basic` `Mathlib.Topology.Algebra.InfiniteSum.Defs` `Mathlib.Topology.Algebra.InfiniteSum.Field` `Mathlib.Topology.Algebra.InfiniteSum.UniformOn` `Mathlib.Topology.Algebra.IntermediateField` `Mathlib.Topology.Algebra.IsUniformGroup.Basic` `Mathlib.Topology.Algebra.IsUniformGroup.Defs` `Mathlib.Topology.Algebra.IsUniformGroup.Order` `Mathlib.Topology.Algebra.LinearTopology` `Mathlib.Topology.Algebra.Localization` `Mathlib.Topology.Algebra.Module.Basic` `Mathlib.Topology.Algebra.Module.Compact` `Mathlib.Topology.Algebra.Module.LinearPMap` `Mathlib.Topology.Algebra.Monoid.AddChar` `Mathlib.Topology.Algebra.Monoid` `Mathlib.Topology.Algebra.MulAction` `Mathlib.Topology.Algebra.MvPolynomial` `Mathlib.Topology.Algebra.NonUnitalAlgebra` `Mathlib.Topology.Algebra.NonUnitalStarAlgebra` `Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology` `Mathlib.Topology.Algebra.Nonarchimedean.Bases` `Mathlib.Topology.Algebra.Nonarchimedean.Basic` `Mathlib.Topology.Algebra.Nonarchimedean.Completion` `Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected` `Mathlib.Topology.Algebra.OpenSubgroup` `Mathlib.Topology.Algebra.Order.Archimedean` `Mathlib.Topology.Algebra.Order.Field` `Mathlib.Topology.Algebra.Order.Floor` `Mathlib.Topology.Algebra.Order.Group` `Mathlib.Topology.Algebra.Order.LiminfLimsup` `Mathlib.Topology.Algebra.Order.Module` `Mathlib.Topology.Algebra.Order.Support` `Mathlib.Topology.Algebra.Order.UpperLower` `Mathlib.Topology.Algebra.ProperAction.Basic` `Mathlib.Topology.Algebra.ProperConstSMul` `Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace` `Mathlib.Topology.Algebra.RestrictedProduct` `Mathlib.Topology.Algebra.Ring.Basic` `Mathlib.Topology.Algebra.Ring.Ideal` `Mathlib.Topology.Algebra.Ring.Real` `Mathlib.Topology.Algebra.Star.Real` `Mathlib.Topology.Algebra.Star.Unitary` `Mathlib.Topology.Algebra.Star` `Mathlib.Topology.Algebra.Support` `Mathlib.Topology.Algebra.TopologicallyNilpotent` `Mathlib.Topology.Algebra.UniformConvergence` `Mathlib.Topology.Algebra.UniformField` `Mathlib.Topology.Algebra.UniformFilterBasis` `Mathlib.Topology.Algebra.UniformMulAction` `Mathlib.Topology.Algebra.UniformRing` `Mathlib.Topology.Algebra.WithZeroTopology` `Mathlib.Topology.ApproximateUnit` `Mathlib.Topology.Bornology.Real` `Mathlib.Topology.Category.CompHausLike.EffectiveEpi` `Mathlib.Topology.Category.Sequential` `Mathlib.Topology.Category.TopCommRingCat` `Mathlib.Topology.Compactness.PseudometrizableLindelof` `Mathlib.Topology.Connected.LocPathConnected` `Mathlib.Topology.Connected.PathComponentOne` `Mathlib.Topology.Connected.PathConnected` `Mathlib.Topology.ContinuousMap.Defs` `Mathlib.Topology.ContinuousMap.Interval` `Mathlib.Topology.ContinuousMap.Ordered` `Mathlib.Topology.Covering` `Mathlib.Topology.Defs.Basic` `Mathlib.Topology.Defs.Filter` `Mathlib.Topology.Defs.Sequences` `Mathlib.Topology.EMetricSpace.Basic` `Mathlib.Topology.EMetricSpace.Defs` `Mathlib.Topology.EMetricSpace.Diam` `Mathlib.Topology.EMetricSpace.Lipschitz` `Mathlib.Topology.EMetricSpace.Paracompact` `Mathlib.Topology.EMetricSpace.Pi` `Mathlib.Topology.FiberBundle.Basic` `Mathlib.Topology.FiberBundle.Constructions` `Mathlib.Topology.FiberBundle.Trivialization` `Mathlib.Topology.Homotopy.Basic` `Mathlib.Topology.Homotopy.Contractible` `Mathlib.Topology.Homotopy.Equiv` `Mathlib.Topology.Homotopy.HSpaces` `Mathlib.Topology.Homotopy.HomotopyGroup` `Mathlib.Topology.Homotopy.Lifting` `Mathlib.Topology.Homotopy.Path` `Mathlib.Topology.Homotopy.Product` `Mathlib.Topology.Instances.CantorSet` `Mathlib.Topology.Instances.Discrete` `Mathlib.Topology.Instances.ENat` `Mathlib.Topology.Instances.Int` `Mathlib.Topology.Instances.Nat` `Mathlib.Topology.Instances.PNat` `Mathlib.Topology.Instances.Rat` `Mathlib.Topology.Instances.Sign` `Mathlib.Topology.Instances.ZMultiples` `Mathlib.Topology.LocallyConstant.Algebra` `Mathlib.Topology.MetricSpace.Antilipschitz` `Mathlib.Topology.MetricSpace.Basic` `Mathlib.Topology.MetricSpace.Bilipschitz` `Mathlib.Topology.MetricSpace.Bounded` `Mathlib.Topology.MetricSpace.CauSeqFilter` `Mathlib.Topology.MetricSpace.Cauchy` `Mathlib.Topology.MetricSpace.Congruence` `Mathlib.Topology.MetricSpace.Defs` `Mathlib.Topology.MetricSpace.DilationEquiv` `Mathlib.Topology.MetricSpace.Dilation` `Mathlib.Topology.MetricSpace.Equicontinuity` `Mathlib.Topology.MetricSpace.Gluing` `Mathlib.Topology.MetricSpace.Infsep` `Mathlib.Topology.MetricSpace.IsometricSMul` `Mathlib.Topology.MetricSpace.Isometry` `Mathlib.Topology.MetricSpace.Lipschitz` `Mathlib.Topology.MetricSpace.MetricSeparated` `Mathlib.Topology.MetricSpace.ProperSpace.Lemmas` `Mathlib.Topology.MetricSpace.ProperSpace.Real` `Mathlib.Topology.MetricSpace.ProperSpace` `Mathlib.Topology.MetricSpace.Pseudo.Basic` `Mathlib.Topology.MetricSpace.Pseudo.Constructions` `Mathlib.Topology.MetricSpace.Pseudo.Defs` `Mathlib.Topology.MetricSpace.Pseudo.Lemmas` `Mathlib.Topology.MetricSpace.Pseudo.Pi` `Mathlib.Topology.MetricSpace.Pseudo.Real` `Mathlib.Topology.MetricSpace.Sequences` `Mathlib.Topology.MetricSpace.ShrinkingLemma` `Mathlib.Topology.MetricSpace.Similarity` `Mathlib.Topology.MetricSpace.Ultra.Basic` `Mathlib.Topology.MetricSpace.Ultra.Pi` `Mathlib.Topology.MetricSpace.Ultra.TotallySeparated` `Mathlib.Topology.Metrizable.Basic` `Mathlib.Topology.Metrizable.CompletelyMetrizable` `Mathlib.Topology.Metrizable.ContinuousMap` `Mathlib.Topology.Metrizable.Real` `Mathlib.Topology.Metrizable.Uniformity` `Mathlib.Topology.Order.Basic` `Mathlib.Topology.Order.Compact` `Mathlib.Topology.Order.CountableSeparating` `Mathlib.Topology.Order.DenselyOrdered` `Mathlib.Topology.Order.ExtendFrom` `Mathlib.Topology.Order.Filter` `Mathlib.Topology.Order.IntermediateValue` `Mathlib.Topology.Order.IsLUB` `Mathlib.Topology.Order.LeftRightLim` `Mathlib.Topology.Order.LeftRightNhds` `Mathlib.Topology.Order.MonotoneContinuity` `Mathlib.Topology.Order.MonotoneConvergence` `Mathlib.Topology.Order.Monotone` `Mathlib.Topology.Order.NhdsSet` `Mathlib.Topology.Order.ProjIcc` `Mathlib.Topology.Order.Real` `Mathlib.Topology.Order.Rolle` `Mathlib.Topology.Order.T5` `Mathlib.Topology.Path` `Mathlib.Topology.Sheaves.Alexandrov` `Mathlib.Topology.Sheaves.Forget` `Mathlib.Topology.Sheaves.Functors` `Mathlib.Topology.Sheaves.Init` `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.CompareReals` `Mathlib.Topology.UniformSpace.DiscreteUniformity` `Mathlib.Topology.UniformSpace.HeineCantor` `Mathlib.Topology.UniformSpace.Matrix` `Mathlib.Topology.UniformSpace.Real` `Mathlib.Topology.UnitInterval` `Mathlib.Util.AddRelatedDecl` `Mathlib.Util.AssertExistsExt` `Mathlib.Util.AssertExists` `Mathlib.Util.AssertNoSorry` `Mathlib.Util.AtomM` `Mathlib.Util.CompileInductive` `Mathlib.Util.CountHeartbeats` `Mathlib.Util.Delaborators` `Mathlib.Util.DischargerAsTactic` `Mathlib.Util.Export` `Mathlib.Util.FormatTable` `Mathlib.Util.GetAllModules` `Mathlib.Util.LongNames` `Mathlib.Util.MemoFix` `Mathlib.Util.Notation3` `Mathlib.Util.PPOptions` `Mathlib.Util.ParseCommand` `Mathlib.Util.Qq` `Mathlib.Util.Simp` `Mathlib.Util.SleepHeartbeats` `Mathlib.Util.Superscript` `Mathlib.Util.SynthesizeUsing` `Mathlib.Util.Tactic` `Mathlib.Util.TermReduce` `Mathlib.Util.TransImports` `Mathlib.Util.WhatsNew` `Mathlib.Util.WithWeakNamespace`	1
8 files `Mathlib.Algebra.EuclideanDomain.Int` `Mathlib.Algebra.Homology.Embedding.Basic` `Mathlib.Algebra.Ring.Int.Defs` `Mathlib.Algebra.Ring.Int.Units` `Mathlib.Data.FP.Basic` `Mathlib.Data.Int.Cast.Field` `Mathlib.Data.Int.ConditionallyCompleteOrder` `Mathlib.Data.Int.LeastGreatest`	2

Declarations diff

+ AddCommGroup.toGrindIntModule
+ AddCommMonoid.toGrindNatModule
+ CommSemiring.toGrindCommSemiring
+ Ring.toGrindRing
+ S1
+ Semiring.toGrindSemiring
+ Semiring.toGrindSemiring_ofNat
+ cast_eq_iff_mod_eq
+ doubleUnderscore
+ eraseIdx_insertIdx_self
+ insertIdx_eraseIdx_self
+ instance (α : Type*) [Semiring α] [IsLeftCancelAdd α] (n : ℕ) [CharP α n] :
+ instance [AddCommMonoid M] [NoZeroSMulDivisors ℕ M] : Lean.Grind.NoNatZeroDivisors M
+ nodup_append'
+ showLinter
- CommRing.toGrindCommRing_ofNat
- doubleUnderscore:
- idxOf_le_length
- idxOf_lt_length_iff
- insertIdx_eraseIdx
- instance (α : Type*) [CommRing α] (n : ℕ) [CharP α n] : Lean.Grind.IsCharP α n
- nodup_append

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.00, 0.01)

Current number	Change	Type
116	-1	adaptation notes

Current commit 4491116737
Reference commit c3b173fdbb

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

* chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * Update lean-toolchain for testing leanprover/lean4#8577 * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8804 * Update lean-toolchain for testing leanprover/lean4#8699 * bump Qq and batteries * meta adaptations * bump aesop * fix * fix (adaptation note) * Update lean-toolchain for leanprover/lean4#8699 * shake * chore: bump to nightly-2025-06-19 * fix * Update lean-toolchain for leanprover/lean4#8699 * fix: correct memoFix's use of unsafe code * fix: adjust noncomputable annotations for new compiler * fix: replace use of `open private _ in` with `open private _ from` The implementation of `open private _ from` relies on specific internals of the old compiler and will no longer work. * remove mul_hmul * chore: adjust one maxHeartbeats for the new compiler * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 * Update lean-toolchain for testing leanprover/lean4#8914 * chore: bump to nightly-2025-06-21 * fix * fixes * fixes * fixes * updated lake manifest * comment out tests * chore: fix for nightly-testing (leanprover-community#26246) * fix * fix * fix grind typeclasses * chore: adaptations for nightly-2025-06-20 * lake update * Update lean-toolchain for leanprover/lean4#8914 * fix grind instance * chore: bump to nightly-2025-06-22 * chore: bump to nightly-2025-06-23 * chore: rm unused `Lean.Util.Paths` import & use updated batteries * Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist) * merge lean-pr-testing-8804 * Bump dependencies and silence linter. * Fixes (Now `elabSimpArgs` already handles `*`, so we can delete the associated code.) * lake update; disable unusedSimpArgs in Batteries * lkae update aesop * disable unusedSimpArgs in MathlibTest * fix grind instance priorities * comment out MathlibTest/zmod with adaptation note * touch for CI * chore: bump to nightly-2025-06-24 * Kick CI * Bump batteries * Guessing adaption for leanprover/lean4#8929 * chore: bump to nightly-2025-06-25 * fix: workflow merging master into nightly-testing * fix * chore: cache get uses tracking remote * touch for new CI * restart CI * chore: bump to nightly-2025-06-26 * Update lean-toolchain for testing leanprover/lean4#8928 * Teach Mathlib about `mrefine` * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8980 * chore: update linter warning test outputs * chore: remove excess line break in deprecation lint now that notes add their own line breaks * chore: more test cleanup * . * cleanup adaptation notes * fix * fix * chore: bump to nightly-2025-06-27 * Merge master into nightly-testing * Merge master into nightly-testing * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * fix tests * chore: bump to nightly-2025-06-28 * Merge master into nightly-testing * lintining * lint --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Rob23oba <101damnations@github.com> Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Cameron Zwarich <cameron@lean-fro.org> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Sebastian Graf <sg@lean-fro.org> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>

* cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * Update lean-toolchain for testing leanprover/lean4#8577 * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8804 * Update lean-toolchain for testing leanprover/lean4#8699 * bump Qq and batteries * meta adaptations * bump aesop * fix * fix (adaptation note) * Update lean-toolchain for leanprover/lean4#8699 * shake * chore: bump to nightly-2025-06-19 * fix * Update lean-toolchain for leanprover/lean4#8699 * fix: correct memoFix's use of unsafe code * fix: adjust noncomputable annotations for new compiler * fix: replace use of `open private _ in` with `open private _ from` The implementation of `open private _ from` relies on specific internals of the old compiler and will no longer work. * remove mul_hmul * chore: adjust one maxHeartbeats for the new compiler * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 * Update lean-toolchain for testing leanprover/lean4#8914 * chore: bump to nightly-2025-06-21 * fix * fixes * fixes * fixes * updated lake manifest * comment out tests * chore: fix for nightly-testing (leanprover-community#26246) * fix * fix * fix grind typeclasses * chore: adaptations for nightly-2025-06-20 * lake update * Update lean-toolchain for leanprover/lean4#8914 * fix grind instance * chore: bump to nightly-2025-06-22 * chore: bump to nightly-2025-06-23 * chore: rm unused `Lean.Util.Paths` import & use updated batteries * Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist) * merge lean-pr-testing-8804 * Bump dependencies and silence linter. * Fixes (Now `elabSimpArgs` already handles `*`, so we can delete the associated code.) * lake update; disable unusedSimpArgs in Batteries * lkae update aesop * disable unusedSimpArgs in MathlibTest * fix grind instance priorities * comment out MathlibTest/zmod with adaptation note * touch for CI * chore: bump to nightly-2025-06-24 * Kick CI * Bump batteries * Guessing adaption for leanprover/lean4#8929 * chore: bump to nightly-2025-06-25 * fix: workflow merging master into nightly-testing * fix * chore: cache get uses tracking remote * touch for new CI * restart CI * chore: bump to nightly-2025-06-26 * Update lean-toolchain for testing leanprover/lean4#8928 * Teach Mathlib about `mrefine` * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8980 * chore: update linter warning test outputs * chore: remove excess line break in deprecation lint now that notes add their own line breaks * chore: more test cleanup * . * cleanup adaptation notes * fix * fix * chore: bump to nightly-2025-06-27 * Merge master into nightly-testing * Merge master into nightly-testing * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * fix tests * chore: bump to nightly-2025-06-28 * Merge master into nightly-testing * lintining * Merge master into nightly-testing * unused simp args * chore: bump to nightly-2025-06-29 * chore: adaptations for nightly-2025-06-29 * Merge master into nightly-testing * chore: robustify `open Mathlib` benchmark * deprecations * Update lean-toolchain for testing leanprover/lean4#9086 * Merge master into nightly-testing * fixes * chore: bump to nightly-2025-06-30 * lake update * lake update * lake update * lake update * lake update * . --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Rob23oba <101damnations@github.com> Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Cameron Zwarich <cameron@lean-fro.org> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Sebastian Graf <sg@lean-fro.org> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>

@Kha

* fix * fixes * chore: adaptations for nightly-2025-06-16 (leanprover-community#25994) * chore: bump to nightly-2025-06-03 * fix * fix * Update lean-toolchain for testing leanprover/lean4#8610 * fix * revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 (leanprover-community#26043) * revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 --------- Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * Update lean-toolchain for testing leanprover/lean4#8577 * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8804 * Update lean-toolchain for testing leanprover/lean4#8699 * bump Qq and batteries * meta adaptations * bump aesop * fix * fix (adaptation note) * Update lean-toolchain for leanprover/lean4#8699 * shake * chore: adaptations for nightly-2025-06-18 (leanprover-community#26077) * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Rob23oba <101damnations@github.com> Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> * chore: bump to nightly-2025-06-19 * feat: add algebra shims for Grind.Nat/IntModule (leanprover-community#26133) This PR adds shims so `grind` will understand Mathlib's `AddCommMonoid` and `AddCommGroup`. (Subsequent shims will connect up the order structures for modules and rings.) * fix * Update lean-toolchain for leanprover/lean4#8699 * fix: correct memoFix's use of unsafe code * fix: adjust noncomputable annotations for new compiler * fix: replace use of `open private _ in` with `open private _ from` The implementation of `open private _ from` relies on specific internals of the old compiler and will no longer work. * remove mul_hmul * chore: adjust one maxHeartbeats for the new compiler * linter * feat: generalize grind algebra shims (leanprover-community#26131) This PR extends the shims converting from Mathlib to `Lean.Grind` typeclasses, now that `grind` knows about (non-commutative)-(semi)-rings. * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 (leanprover-community#26209) * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * chore: bump to nightly-2025-06-19 * fix * remove mul_hmul * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Rob23oba <101damnations@github.com> Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> * Update lean-toolchain for testing leanprover/lean4#8914 * chore: bump to nightly-2025-06-21 * fix * fixes * fixes * fixes * updated lake manifest * comment out tests * chore: fix for nightly-testing (leanprover-community#26246) * fix * fix * fix grind typeclasses * chore: adaptations for nightly-2025-06-20 * lake update * Update lean-toolchain for leanprover/lean4#8914 * fix grind instance * chore: bump to nightly-2025-06-22 * chore: bump to nightly-2025-06-23 * chore: rm unused `Lean.Util.Paths` import & use updated batteries * Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist) * merge lean-pr-testing-8804 * Bump dependencies and silence linter. * Fixes (Now `elabSimpArgs` already handles `*`, so we can delete the associated code.) * lake update; disable unusedSimpArgs in Batteries * lkae update aesop * disable unusedSimpArgs in MathlibTest * fix grind instance priorities * comment out MathlibTest/zmod with adaptation note * touch for CI * chore: bump to nightly-2025-06-24 * Kick CI * Bump batteries * Guessing adaption for leanprover/lean4#8929 * chore: bump to nightly-2025-06-25 * fix: workflow merging master into nightly-testing * fix * chore: cache get uses tracking remote * touch for new CI * restart CI * chore: bump to nightly-2025-06-26 * Update lean-toolchain for testing leanprover/lean4#8928 * Teach Mathlib about `mrefine` * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8980 * chore: update linter warning test outputs * chore: remove excess line break in deprecation lint now that notes add their own line breaks * chore: more test cleanup * . * cleanup adaptation notes * fix * fix * chore: bump to nightly-2025-06-27 * chore: adaptations for nightly-2025-06-26 (#2) * Merge master into nightly-testing * Merge master into nightly-testing * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * chore: adaptations for nightly-2025-06-27 (#3) * fix tests * chore: bump to nightly-2025-06-28 * Merge master into nightly-testing * lintining * Merge master into nightly-testing * unused simp args * chore: bump to nightly-2025-06-29 * chore: adaptations for nightly-2025-06-29 * chore: adaptations for nightly-2025-06-28 (#5) * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * Update lean-toolchain for testing leanprover/lean4#8577 * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8804 * Update lean-toolchain for testing leanprover/lean4#8699 * bump Qq and batteries * meta adaptations * bump aesop * fix * fix (adaptation note) * Update lean-toolchain for leanprover/lean4#8699 * shake * chore: bump to nightly-2025-06-19 * fix * Update lean-toolchain for leanprover/lean4#8699 * fix: correct memoFix's use of unsafe code * fix: adjust noncomputable annotations for new compiler * fix: replace use of `open private _ in` with `open private _ from` The implementation of `open private _ from` relies on specific internals of the old compiler and will no longer work. * remove mul_hmul * chore: adjust one maxHeartbeats for the new compiler * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 * Update lean-toolchain for testing leanprover/lean4#8914 * chore: bump to nightly-2025-06-21 * fix * fixes * fixes * fixes * updated lake manifest * comment out tests * chore: fix for nightly-testing (leanprover-community#26246) * fix * fix * fix grind typeclasses * chore: adaptations for nightly-2025-06-20 * lake update * Update lean-toolchain for leanprover/lean4#8914 * fix grind instance * chore: bump to nightly-2025-06-22 * chore: bump to nightly-2025-06-23 * chore: rm unused `Lean.Util.Paths` import & use updated batteries * Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist) * merge lean-pr-testing-8804 * Bump dependencies and silence linter. * Fixes (Now `elabSimpArgs` already handles `*`, so we can delete the associated code.) * lake update; disable unusedSimpArgs in Batteries * lkae update aesop * disable unusedSimpArgs in MathlibTest * fix grind instance priorities * comment out MathlibTest/zmod with adaptation note * touch for CI * chore: bump to nightly-2025-06-24 * Kick CI * Bump batteries * Guessing adaption for leanprover/lean4#8929 * chore: bump to nightly-2025-06-25 * fix: workflow merging master into nightly-testing * fix * chore: cache get uses tracking remote * touch for new CI * restart CI * chore: bump to nightly-2025-06-26 * Update lean-toolchain for testing leanprover/lean4#8928 * Teach Mathlib about `mrefine` * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8980 * chore: update linter warning test outputs * chore: remove excess line break in deprecation lint now that notes add their own line breaks * chore: more test cleanup * . * cleanup adaptation notes * fix * fix * chore: bump to nightly-2025-06-27 * Merge master into nightly-testing * Merge master into nightly-testing * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * fix tests * chore: bump to nightly-2025-06-28 * Merge master into nightly-testing * lintining * lint --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Rob23oba <101damnations@github.com> Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Cameron Zwarich <cameron@lean-fro.org> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Sebastian Graf <sg@lean-fro.org> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com> * Merge master into nightly-testing * chore: robustify `open Mathlib` benchmark * deprecations * Update lean-toolchain for testing leanprover/lean4#9086 * Merge master into nightly-testing * fixes * chore: bump to nightly-2025-06-30 * lake update * lake update * lake update * lake update * lake update * . * Merge master into nightly-testing * Merge master into nightly-testing * Merge master into nightly-testing * Merge master into nightly-testing * cleanup * unusedSimpArgs * bump toolchain * lake update * Merge master into nightly-testing * Merge master into nightly-testing * chore: adaptations for nightly-2025-07-01 * add adaptation note * add adaptation note * chore: bump to nightly-2025-07-02 * fixes * Merge master into nightly-testing * fixes * update test output * Merge master into nightly-testing * Merge master into nightly-testing * chore: bump to nightly-2025-07-03 * chore: adaptations for nightly-2025-07-03 --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Rob23oba <101damnations@github.com> Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Cameron Zwarich <cameron@lean-fro.org> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Sebastian Graf <sg@lean-fro.org> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>

fix

8f6f64d

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jun 21, 2025

fix

4491116

kim-em merged commit f757b4f into leanprover-community:nightly-testing Jun 22, 2025
9 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

chore: fix for nightly-testing#26246

chore: fix for nightly-testing#26246
kim-em merged 2 commits intoleanprover-community:nightly-testingfrom
Rob23oba:nightly-testing

Rob23oba commented Jun 21, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Jun 21, 2025 •

edited

Loading

Declarations diff

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

Rob23oba commented Jun 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jun 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary c3b173fdbb

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Rob23oba commented Jun 21, 2025 •

edited

Loading

github-actions bot commented Jun 21, 2025 •

edited

Loading