[Merged by Bors] - feat(Order): relate chains to antichains by b-mehta · Pull Request #20756 · leanprover-community/mathlib4

b-mehta · 2025-01-14T22:18:09Z

A set which is a chain and an antichain is subsingleton. As a result, the intersection of a chain and antichain is subsingleton.

Useful from the disproof of the Aharoni–Korman conjecture, #20082.

I believe the large import here is acceptable, as IsChain and IsAntichain need to be related to each other somewhere, but there is not much to say about both (as this PR shows). As such, making a third file specifically for these seems unnecessary, and putting these in Order.Chain results in a larger import change.

github-actions · 2025-01-14T22:19:00Z

messageFile.md

vihdzp

I'm surprised we weren't already defining IsAntichain r s as IsChain rᶜ s, I completely agree with the import increase.

Mathlib/Order/Antichain.lean

YaelDillies · 2025-01-17T09:50:59Z

I do think we should do something about the new imports. I will investigate

YaelDillies · 2025-01-22T23:11:32Z

Okay, I see many ways to get rid of the import increase, so I think this PR can move forward.

maintainer merge

github-actions · 2025-01-22T23:11:53Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

jcommelin · 2025-01-23T05:46:22Z

Thanks 🎉

bors merge

A set which is a chain and an antichain is subsingleton. As a result, the intersection of a chain and antichain is subsingleton. Useful from the disproof of the Aharoni–Korman conjecture, #20082. I believe the large import here is acceptable, as `IsChain` and `IsAntichain` need to be related to each other somewhere, but there is not much to say about both (as this PR shows). As such, making a third file specifically for these seems unnecessary, and putting these in `Order.Chain` results in a larger import change.

mathlib-bors · 2025-01-23T06:28:37Z

Build failed (retrying...):

Build

A set which is a chain and an antichain is subsingleton. As a result, the intersection of a chain and antichain is subsingleton. Useful from the disproof of the Aharoni–Korman conjecture, #20082. I believe the large import here is acceptable, as `IsChain` and `IsAntichain` need to be related to each other somewhere, but there is not much to say about both (as this PR shows). As such, making a third file specifically for these seems unnecessary, and putting these in `Order.Chain` results in a larger import change.

mathlib-bors · 2025-01-23T07:41:55Z

Pull request successfully merged into master.

Build succeeded:

adomani · 2025-01-27T17:24:49Z

There was a question on Zulip about what was the import diff for this PR. As far as I can tell, below is the import diff between

8bec620

and

f28d136

Import changes for all files

Files	Import difference
407 files `Mathlib.Algebra.Algebra.Basic` `Mathlib.Algebra.Algebra.Equiv` `Mathlib.Algebra.Algebra.Field` `Mathlib.Algebra.Algebra.Hom.Rat` `Mathlib.Algebra.Algebra.Hom` `Mathlib.Algebra.Algebra.NonUnitalHom` `Mathlib.Algebra.Algebra.Opposite` `Mathlib.Algebra.Algebra.Pi` `Mathlib.Algebra.Algebra.Prod` `Mathlib.Algebra.BigOperators.Associated` `Mathlib.Algebra.BigOperators.Finsupp` `Mathlib.Algebra.BigOperators.Sym` `Mathlib.Algebra.Category.Grp.Biproducts` `Mathlib.Algebra.Category.Grp.Colimits` `Mathlib.Algebra.Category.Grp.FilteredColimits` `Mathlib.Algebra.Category.Grp.Limits` `Mathlib.Algebra.Category.ModuleCat.Colimits` `Mathlib.Algebra.Category.ModuleCat.FilteredColimits` `Mathlib.Algebra.Category.MonCat.FilteredColimits` `Mathlib.Algebra.Category.MonCat.Limits` `Mathlib.Algebra.Category.Ring.FilteredColimits` `Mathlib.Algebra.Category.Ring.Limits` `Mathlib.Algebra.Colimit.DirectLimit` `Mathlib.Algebra.DirectSum.AddChar` `Mathlib.Algebra.DirectSum.Basic` `Mathlib.Algebra.DirectSum.Ring` `Mathlib.Algebra.Equiv.TransferInstance` `Mathlib.Algebra.Field.Subfield.Basic` `Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra` `Mathlib.Algebra.GradedMonoid` `Mathlib.Algebra.GradedMulAction` `Mathlib.Algebra.Group.AddChar` `Mathlib.Algebra.Group.ForwardDiff` `Mathlib.Algebra.Group.Subgroup.Finsupp` `Mathlib.Algebra.Group.Subgroup.Order` `Mathlib.Algebra.Group.Subgroup.Pointwise` `Mathlib.Algebra.Group.Submonoid.BigOperators` `Mathlib.Algebra.Group.Submonoid.Finsupp` `Mathlib.Algebra.Group.Submonoid.Pointwise` `Mathlib.Algebra.Group.Submonoid.Units` `Mathlib.Algebra.Homology.Embedding.CochainComplex` `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.StupidTrunc` `Mathlib.Algebra.Homology.Embedding.TruncGEHomology` `Mathlib.Algebra.Homology.Embedding.TruncGE` `Mathlib.Algebra.Homology.Embedding.TruncLE` `Mathlib.Algebra.Homology.ExactSequence` `Mathlib.Algebra.Homology.Factorizations.Basic` `Mathlib.Algebra.Homology.HomologicalComplexAbelian` `Mathlib.Algebra.Homology.HomologySequenceLemmas` `Mathlib.Algebra.Homology.HomologySequence` `Mathlib.Algebra.Homology.HomotopyCategory` `Mathlib.Algebra.Homology.HomotopyCofiber` `Mathlib.Algebra.Homology.Homotopy` `Mathlib.Algebra.Homology.Localization` `Mathlib.Algebra.Homology.Opposite` `Mathlib.Algebra.Homology.QuasiIso` `Mathlib.Algebra.Homology.Refinements` `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.Lie.Basic` `Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra` `Mathlib.Algebra.Module.Submodule.Basic` `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.Map` `Mathlib.Algebra.Module.Submodule.Range` `Mathlib.Algebra.Module.Submodule.RestrictScalars` `Mathlib.Algebra.MonoidAlgebra.Basic` `Mathlib.Algebra.MonoidAlgebra.Defs` `Mathlib.Algebra.MonoidAlgebra.Degree` `Mathlib.Algebra.MonoidAlgebra.Division` `Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors` `Mathlib.Algebra.MonoidAlgebra.Support` `Mathlib.Algebra.Order.Antidiag.Finsupp` `Mathlib.Algebra.Order.Antidiag.Nat` `Mathlib.Algebra.Order.Antidiag.Pi` `Mathlib.Algebra.Order.Archimedean.Submonoid` `Mathlib.Algebra.Order.Floor.Div` `Mathlib.Algebra.Order.Interval.Basic` `Mathlib.Algebra.Order.Star.Conjneg` `Mathlib.Algebra.Order.UpperLower` `Mathlib.Algebra.Pointwise.Stabilizer` `Mathlib.Algebra.Polynomial.Basic` `Mathlib.Algebra.Polynomial.BigOperators` `Mathlib.Algebra.Polynomial.CancelLeads` `Mathlib.Algebra.Polynomial.Coeff` `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.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.HasseDeriv` `Mathlib.Algebra.Polynomial.Identities` `Mathlib.Algebra.Polynomial.Inductions` `Mathlib.Algebra.Polynomial.Mirror` `Mathlib.Algebra.Polynomial.Monic` `Mathlib.Algebra.Polynomial.Monomial` `Mathlib.Algebra.Polynomial.Reverse` `Mathlib.Algebra.Polynomial.UnitTrinomial` `Mathlib.Algebra.Ring.CentroidHom` `Mathlib.Algebra.Ring.Semireal.Defs` `Mathlib.Algebra.Ring.Subring.Basic` `Mathlib.Algebra.Ring.Subring.MulOpposite` `Mathlib.Algebra.Ring.Subring.Pointwise` `Mathlib.Algebra.Ring.Subsemiring.Basic` `Mathlib.Algebra.Ring.Subsemiring.MulOpposite` `Mathlib.Algebra.Ring.Subsemiring.Pointwise` `Mathlib.Algebra.Ring.SumsOfSquares` `Mathlib.Algebra.SkewMonoidAlgebra.Basic` `Mathlib.Algebra.Small.Group` `Mathlib.Algebra.Small.Module` `Mathlib.Algebra.Small.Ring` `Mathlib.Algebra.Squarefree.Basic` `Mathlib.Algebra.Star.CentroidHom` `Mathlib.Algebra.Star.Conjneg` `Mathlib.Algebra.Star.StarAlgHom` `Mathlib.Algebra.Star.Subsemiring` `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.MooreComplex` `Mathlib.AlgebraicTopology.Quasicategory.Basic` `Mathlib.AlgebraicTopology.Quasicategory.Nerve` `Mathlib.AlgebraicTopology.Quasicategory.StrictSegal` `Mathlib.AlgebraicTopology.SimplexCategory` `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.Coskeletal` `Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat` `Mathlib.AlgebraicTopology.SimplicialSet.KanComplex` `Mathlib.AlgebraicTopology.SimplicialSet.Monoidal` `Mathlib.AlgebraicTopology.SimplicialSet.Nerve` `Mathlib.AlgebraicTopology.SimplicialSet.Path` `Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal` `Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four` `Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel` `Mathlib.CategoryTheory.Abelian.Exact` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory` `Mathlib.CategoryTheory.Abelian.InjectiveResolution` `Mathlib.CategoryTheory.Abelian.LeftDerived` `Mathlib.CategoryTheory.Abelian.Opposite` `Mathlib.CategoryTheory.Abelian.ProjectiveResolution` `Mathlib.CategoryTheory.Abelian.Refinements` `Mathlib.CategoryTheory.Abelian.RightDerived` `Mathlib.CategoryTheory.Abelian.Transfer` `Mathlib.CategoryTheory.Action.Concrete` `Mathlib.CategoryTheory.Action.Limits` `Mathlib.CategoryTheory.Action.Monoidal` `Mathlib.CategoryTheory.Adjunction.Additive` `Mathlib.CategoryTheory.Generator.Abelian` `Mathlib.CategoryTheory.Generator.Preadditive` `Mathlib.CategoryTheory.Idempotents.SimplicialObject` `Mathlib.CategoryTheory.Linear.Yoneda` `Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive` `Mathlib.CategoryTheory.Monoidal.Tor` `Mathlib.CategoryTheory.Noetherian` `Mathlib.CategoryTheory.Preadditive.InjectiveResolution` `Mathlib.CategoryTheory.Preadditive.Opposite` `Mathlib.CategoryTheory.Preadditive.ProjectiveResolution` `Mathlib.CategoryTheory.Preadditive.Yoneda.Basic` `Mathlib.CategoryTheory.Preadditive.Yoneda.Projective` `Mathlib.CategoryTheory.Shift.Opposite` `Mathlib.CategoryTheory.Shift.ShiftedHomOpposite` `Mathlib.CategoryTheory.Simple` `Mathlib.CategoryTheory.Sites.Abelian` `Mathlib.CategoryTheory.Triangulated.Opposite.Basic` `Mathlib.CategoryTheory.Triangulated.Opposite.Triangle` `Mathlib.Combinatorics.Additive.AP.Three.Defs` `Mathlib.Combinatorics.Additive.Corner.Defs` `Mathlib.Combinatorics.Additive.FreimanHom` `Mathlib.Combinatorics.Colex` `Mathlib.Combinatorics.Derangements.Basic` `Mathlib.Combinatorics.Derangements.Finite` `Mathlib.Combinatorics.Enumerative.Bell` `Mathlib.Combinatorics.SetFamily.AhlswedeZhang` `Mathlib.Combinatorics.SetFamily.Compression.UV` `Mathlib.Combinatorics.SetFamily.FourFunctions` `Mathlib.Combinatorics.SetFamily.HarrisKleitman` `Mathlib.Combinatorics.SetFamily.Intersecting` `Mathlib.Combinatorics.SetFamily.Kleitman` `Mathlib.Combinatorics.SetFamily.KruskalKatona` `Mathlib.Combinatorics.SetFamily.LYM` `Mathlib.Combinatorics.SetFamily.Shadow` `Mathlib.Combinatorics.SimpleGraph.Acyclic` `Mathlib.Combinatorics.SimpleGraph.Circulant` `Mathlib.Combinatorics.SimpleGraph.Clique` `Mathlib.Combinatorics.SimpleGraph.Coloring` `Mathlib.Combinatorics.SimpleGraph.ConcreteColorings` `Mathlib.Combinatorics.SimpleGraph.Density` `Mathlib.Combinatorics.SimpleGraph.Diam` `Mathlib.Combinatorics.SimpleGraph.Finite` `Mathlib.Combinatorics.SimpleGraph.Girth` `Mathlib.Combinatorics.SimpleGraph.Hamiltonian` `Mathlib.Combinatorics.SimpleGraph.Hasse` `Mathlib.Combinatorics.SimpleGraph.IncMatrix` `Mathlib.Combinatorics.SimpleGraph.Metric` `Mathlib.Combinatorics.SimpleGraph.Operations` `Mathlib.Combinatorics.SimpleGraph.Partition` `Mathlib.Combinatorics.SimpleGraph.Path` `Mathlib.Combinatorics.SimpleGraph.Prod` `Mathlib.Combinatorics.SimpleGraph.Regularity.Energy` `Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise` `Mathlib.Combinatorics.SimpleGraph.Subgraph` `Mathlib.Combinatorics.SimpleGraph.Trails` `Mathlib.Combinatorics.SimpleGraph.Triangle.Basic` `Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite` `Mathlib.Combinatorics.SimpleGraph.Turan` `Mathlib.Combinatorics.Young.SemistandardTableau` `Mathlib.Combinatorics.Young.YoungDiagram` `Mathlib.Data.Complex.Basic` `Mathlib.Data.Complex.BigOperators` `Mathlib.Data.DFinsupp.BigOperators` `Mathlib.Data.DFinsupp.Interval` `Mathlib.Data.DFinsupp.Multiset` `Mathlib.Data.DFinsupp.Submonoid` `Mathlib.Data.Finset.Finsupp` `Mathlib.Data.Finset.Grade` `Mathlib.Data.Finset.Interval` `Mathlib.Data.Finset.Sups` `Mathlib.Data.Finsupp.AList` `Mathlib.Data.Finsupp.Antidiagonal` `Mathlib.Data.Finsupp.Basic` `Mathlib.Data.Finsupp.Encodable` `Mathlib.Data.Finsupp.Ext` `Mathlib.Data.Finsupp.Interval` `Mathlib.Data.Finsupp.Lex` `Mathlib.Data.Finsupp.Multiset` `Mathlib.Data.Finsupp.Order` `Mathlib.Data.Finsupp.PWO` `Mathlib.Data.Finsupp.ToDFinsupp` `Mathlib.Data.Finsupp.Weight` `Mathlib.Data.Fintype.Order` `Mathlib.Data.Matrix.Basic` `Mathlib.Data.Matrix.Basis` `Mathlib.Data.Matrix.Composition` `Mathlib.Data.Multiset.Interval` `Mathlib.Data.NNReal.Star` `Mathlib.Data.Nat.Cast.SetInterval` `Mathlib.Data.Nat.Choose.Cast` `Mathlib.Data.Nat.Choose.Factorization` `Mathlib.Data.Nat.Choose.Multinomial` `Mathlib.Data.Nat.Choose.Vandermonde` `Mathlib.Data.Nat.Factorial.Cast` `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.Squarefree` `Mathlib.Data.Rat.Star` `Mathlib.Data.Real.Star` `Mathlib.Data.Set.Sups` `Mathlib.Data.Setoid.Partition` `Mathlib.Data.Sym.Card` `Mathlib.Geometry.Group.Growth.LinearLowerBound` `Mathlib.Geometry.Group.Growth.QuotientInter` `Mathlib.GroupTheory.ArchimedeanDensely` `Mathlib.GroupTheory.Archimedean` `Mathlib.GroupTheory.Divisible` `Mathlib.GroupTheory.DoubleCoset` `Mathlib.GroupTheory.GroupAction.Quotient` `Mathlib.GroupTheory.Perm.ClosureSwap` `Mathlib.GroupTheory.Perm.Option` `Mathlib.GroupTheory.Perm.Sign` `Mathlib.GroupTheory.QuotientGroup.Basic` `Mathlib.GroupTheory.Subgroup.Simple` `Mathlib.GroupTheory.Submonoid.Inverses` `Mathlib.LinearAlgebra.BilinearMap` `Mathlib.LinearAlgebra.Countable` `Mathlib.LinearAlgebra.Finsupp.Defs` `Mathlib.LinearAlgebra.Finsupp.LSum` `Mathlib.LinearAlgebra.Finsupp.LinearCombination` `Mathlib.LinearAlgebra.Finsupp.Pi` `Mathlib.LinearAlgebra.Finsupp.SumProd` `Mathlib.LinearAlgebra.Finsupp.Supported` `Mathlib.LinearAlgebra.Matrix.SemiringInverse` `Mathlib.LinearAlgebra.Multilinear.Basic` `Mathlib.LinearAlgebra.Multilinear.Pi` `Mathlib.LinearAlgebra.Pi` `Mathlib.LinearAlgebra.SModEq` `Mathlib.LinearAlgebra.Span.Defs` `Mathlib.Logic.Equiv.Fintype` `Mathlib.Logic.Hydra` `Mathlib.MeasureTheory.Constructions.AddChar` `Mathlib.MeasureTheory.Constructions.Cylinders` `Mathlib.MeasureTheory.Constructions.SubmoduleQuotient` `Mathlib.MeasureTheory.MeasurableSpace.Basic` `Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated` `Mathlib.MeasureTheory.MeasurableSpace.Embedding` `Mathlib.MeasureTheory.MeasurableSpace.Pi` `Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict` `Mathlib.MeasureTheory.MeasurableSpace.Prod` `Mathlib.NumberTheory.ArithmeticFunction` `Mathlib.NumberTheory.ClassNumber.AdmissibleAbs` `Mathlib.NumberTheory.MaricaSchoenheim` `Mathlib.NumberTheory.Primorial` `Mathlib.NumberTheory.SmoothNumbers` `Mathlib.Order.Atoms.Finite` `Mathlib.Order.Atoms` `Mathlib.Order.Birkhoff` `Mathlib.Order.Category.FinBddDistLat` `Mathlib.Order.Category.FinBoolAlg` `Mathlib.Order.Category.NonemptyFinLinOrd` `Mathlib.Order.DirectedInverseSystem` `Mathlib.Order.InitialSeg` `Mathlib.Order.KonigLemma` `Mathlib.Order.KrullDimension` `Mathlib.Order.Minimal` `Mathlib.Order.Partition.Equipartition` `Mathlib.Order.Partition.Finpartition` `Mathlib.Order.Radical` `Mathlib.Order.SuccPred.InitialSeg` `Mathlib.Order.SuccPred.Tree` `Mathlib.Order.UpperLower.Basic` `Mathlib.Order.UpperLower.Hom` `Mathlib.Order.UpperLower.LocallyFinite` `Mathlib.RingTheory.ChainOfDivisors` `Mathlib.RingTheory.Ideal.BigOperators` `Mathlib.RingTheory.Ideal.Lattice` `Mathlib.RingTheory.Ideal.Prime` `Mathlib.RingTheory.Localization.Integer` `Mathlib.RingTheory.Nilpotent.Basic` `Mathlib.RingTheory.NonUnitalSubring.Basic` `Mathlib.RingTheory.Polynomial.Hermite.Basic` `Mathlib.RingTheory.Polynomial.Opposites` `Mathlib.RingTheory.Polynomial.Pochhammer` `Mathlib.RingTheory.Radical` `Mathlib.RingTheory.SimpleRing.Basic` `Mathlib.RingTheory.SimpleRing.Defs` `Mathlib.RingTheory.SimpleRing.Field` `Mathlib.RingTheory.Spectrum.Prime.Defs` `Mathlib.RingTheory.TwoSidedIdeal.Operations` `Mathlib.RingTheory.UniqueFactorizationDomain.Basic` `Mathlib.RingTheory.UniqueFactorizationDomain.Defs` `Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet` `Mathlib.RingTheory.UniqueFactorizationDomain.Finite` `Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp` `Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid` `Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative` `Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity` `Mathlib.RingTheory.UniqueFactorizationDomain.Nat` `Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors` `Mathlib.Tactic.ComputeDegree` `Mathlib.Testing.Plausible.Functions` `Mathlib.Topology.Exterior` `Mathlib.Topology.Inseparable` `Mathlib.adomaniLeanUtils.Rev` `Mathlib.adomaniLeanUtils.all_tactics` `Mathlib.adomaniLeanUtils.move_add_short_test` `Mathlib.adomaniLeanUtils.move_add_utils` `Mathlib.adomaniLeanUtils.to_left_right`	1
322 files `Mathlib.Algebra.AddConstMap.Basic` `Mathlib.Algebra.AddConstMap.Equiv` `Mathlib.Algebra.BigOperators.Balance` `Mathlib.Algebra.BigOperators.Expect` `Mathlib.Algebra.BigOperators.Fin` `Mathlib.Algebra.BigOperators.Finprod` `Mathlib.Algebra.BigOperators.Group.Finset.Basic` `Mathlib.Algebra.BigOperators.GroupWithZero.Action` `Mathlib.Algebra.BigOperators.GroupWithZero.Finset` `Mathlib.Algebra.BigOperators.Intervals` `Mathlib.Algebra.BigOperators.Module` `Mathlib.Algebra.BigOperators.NatAntidiagonal` `Mathlib.Algebra.BigOperators.Option` `Mathlib.Algebra.BigOperators.Pi` `Mathlib.Algebra.BigOperators.Ring.Nat` `Mathlib.Algebra.BigOperators.Ring` `Mathlib.Algebra.BigOperators.WithTop` `Mathlib.Algebra.Category.Grp.ZModuleEquivalence` `Mathlib.Algebra.Category.ModuleCat.Basic` `Mathlib.Algebra.CharP.ExpChar` `Mathlib.Algebra.CharP.Lemmas` `Mathlib.Algebra.CharP.Reduced` `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.GeomSum` `Mathlib.Algebra.Group.EvenFunction` `Mathlib.Algebra.Group.Pointwise.Finset.Basic` `Mathlib.Algebra.Group.Pointwise.Finset.Interval` `Mathlib.Algebra.Group.Pointwise.Set.BigOperators` `Mathlib.Algebra.Group.Translate` `Mathlib.Algebra.Group.UniqueProds.Basic` `Mathlib.Algebra.GroupWithZero.Pointwise.Finset` `Mathlib.Algebra.Homology.Additive` `Mathlib.Algebra.Homology.CommSq` `Mathlib.Algebra.Homology.Embedding.Restriction` `Mathlib.Algebra.Homology.HomologicalComplexBiprod` `Mathlib.Algebra.Homology.Linear` `Mathlib.Algebra.Homology.ShortComplex.Abelian` `Mathlib.Algebra.Homology.Square` `Mathlib.Algebra.Module.BigOperators` `Mathlib.Algebra.Module.LinearMap.Rat` `Mathlib.Algebra.Module.Rat` `Mathlib.Algebra.Order.Archimedean.Basic` `Mathlib.Algebra.Order.Archimedean.Hom` `Mathlib.Algebra.Order.BigOperators.Expect` `Mathlib.Algebra.Order.BigOperators.Group.Finset` `Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite` `Mathlib.Algebra.Order.BigOperators.Ring.Finset` `Mathlib.Algebra.Order.CauSeq.BigOperators` `Mathlib.Algebra.Order.CompleteField` `Mathlib.Algebra.Order.Disjointed` `Mathlib.Algebra.Order.Field.Rat` `Mathlib.Algebra.Order.Floor` `Mathlib.Algebra.Order.Group.Indicator` `Mathlib.Algebra.Order.Group.Pointwise.Interval` `Mathlib.Algebra.Order.Interval.Multiset` `Mathlib.Algebra.Order.Module.Rat` `Mathlib.Algebra.Order.Nonneg.Field` `Mathlib.Algebra.Order.Nonneg.Floor` `Mathlib.Algebra.Order.Nonneg.Lattice` `Mathlib.Algebra.Order.Nonneg.Module` `Mathlib.Algebra.Order.Nonneg.Ring` `Mathlib.Algebra.Order.PartialSups` `Mathlib.Algebra.Order.Rearrangement` `Mathlib.Algebra.Order.Round` `Mathlib.Algebra.Order.SuccPred.TypeTags` `Mathlib.Algebra.Order.SuccPred.WithBot` `Mathlib.Algebra.Order.SuccPred` `Mathlib.Algebra.Ring.Divisibility.Lemmas` `Mathlib.Algebra.Ring.Pointwise.Finset` `Mathlib.Algebra.Tropical.BigOperators` `Mathlib.Analysis.Normed.Group.Seminorm` `Mathlib.CategoryTheory.Abelian.Basic` `Mathlib.CategoryTheory.Abelian.FunctorCategory` `Mathlib.CategoryTheory.Abelian.Subobject` `Mathlib.CategoryTheory.Generator.Sheaf` `Mathlib.CategoryTheory.Idempotents.Basic` `Mathlib.CategoryTheory.Idempotents.Biproducts` `Mathlib.CategoryTheory.Idempotents.FunctorCategories` `Mathlib.CategoryTheory.Idempotents.FunctorExtension` `Mathlib.CategoryTheory.Idempotents.HomologicalComplex` `Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi` `Mathlib.CategoryTheory.Idempotents.Karoubi` `Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures` `Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous` `Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct` `Mathlib.CategoryTheory.Linear.FunctorCategory` `Mathlib.CategoryTheory.Linear.LinearFunctor` `Mathlib.CategoryTheory.Localization.SmallShiftedHom` `Mathlib.CategoryTheory.Monoidal.Linear` `Mathlib.CategoryTheory.Monoidal.Preadditive` `Mathlib.CategoryTheory.Monoidal.Subcategory` `Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition` `Mathlib.CategoryTheory.Preadditive.AdditiveFunctor` `Mathlib.CategoryTheory.Preadditive.Biproducts` `Mathlib.CategoryTheory.Preadditive.EilenbergMoore` `Mathlib.CategoryTheory.Preadditive.EndoFunctor` `Mathlib.CategoryTheory.Preadditive.FunctorCategory` `Mathlib.CategoryTheory.Preadditive.LeftExact` `Mathlib.CategoryTheory.Preadditive.Mat` `Mathlib.CategoryTheory.Quotient.Linear` `Mathlib.CategoryTheory.Quotient.Preadditive` `Mathlib.CategoryTheory.Shift.InducedShiftSequence` `Mathlib.CategoryTheory.Shift.Pullback` `Mathlib.CategoryTheory.Shift.ShiftSequence` `Mathlib.CategoryTheory.Shift.ShiftedHom` `Mathlib.CategoryTheory.Sites.Adjunction` `Mathlib.CategoryTheory.Sites.Canonical` `Mathlib.CategoryTheory.Sites.CartesianClosed` `Mathlib.CategoryTheory.Sites.ChosenFiniteProducts` `Mathlib.CategoryTheory.Sites.CompatiblePlus` `Mathlib.CategoryTheory.Sites.CompatibleSheafification` `Mathlib.CategoryTheory.Sites.ConcreteSheafification` `Mathlib.CategoryTheory.Sites.Continuous` `Mathlib.CategoryTheory.Sites.CoverLifting` `Mathlib.CategoryTheory.Sites.CoverPreserving` `Mathlib.CategoryTheory.Sites.Coverage` `Mathlib.CategoryTheory.Sites.CoversTop` `Mathlib.CategoryTheory.Sites.IsSheafOneHypercover` `Mathlib.CategoryTheory.Sites.Limits` `Mathlib.CategoryTheory.Sites.Localization` `Mathlib.CategoryTheory.Sites.OneHypercover` `Mathlib.CategoryTheory.Sites.Over` `Mathlib.CategoryTheory.Sites.Plus` `Mathlib.CategoryTheory.Sites.PreservesSheafification` `Mathlib.CategoryTheory.Sites.SheafHom` `Mathlib.CategoryTheory.Sites.Sheaf` `Mathlib.CategoryTheory.Sites.Sheafification` `Mathlib.CategoryTheory.Sites.Subcanonical` `Mathlib.CategoryTheory.Sites.Types` `Mathlib.CategoryTheory.Sites.Whiskering` `Mathlib.CategoryTheory.SmallObject.Iteration.Basic` `Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc` `Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone` `Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty` `Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom` `Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting` `Mathlib.CategoryTheory.SmallObject.WellOrderInductionData` `Mathlib.CategoryTheory.Triangulated.Rotate` `Mathlib.Combinatorics.Additive.CovBySMul` `Mathlib.Combinatorics.Additive.Dissociation` `Mathlib.Combinatorics.Additive.DoublingConst` `Mathlib.Combinatorics.Additive.ETransform` `Mathlib.Combinatorics.Additive.Energy` `Mathlib.Combinatorics.Additive.PluenneckeRuzsa` `Mathlib.Combinatorics.Additive.SmallTripling` `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.HalesJewett` `Mathlib.Combinatorics.Pigeonhole` `Mathlib.Combinatorics.Schnirelmann` `Mathlib.Combinatorics.SetFamily.Shatter` `Mathlib.Computability.Ackermann` `Mathlib.Computability.DFA` `Mathlib.Computability.EpsilonNFA` `Mathlib.Computability.MyhillNerode` `Mathlib.Computability.NFA` `Mathlib.Data.DFinsupp.Lex` `Mathlib.Data.DFinsupp.Notation` `Mathlib.Data.ENNReal.Basic` `Mathlib.Data.ENNReal.Inv` `Mathlib.Data.ENNReal.Lemmas` `Mathlib.Data.ENNReal.Operations` `Mathlib.Data.ENNReal.Real` `Mathlib.Data.ENat.Basic` `Mathlib.Data.ENat.BigOperators` `Mathlib.Data.ENat.Lattice` `Mathlib.Data.Fin.SuccPred` `Mathlib.Data.Fin.Tuple.BubbleSortInduction` `Mathlib.Data.Fin.Tuple.NatAntidiagonal` `Mathlib.Data.Fin.Tuple.Reflection` `Mathlib.Data.Fin.Tuple.Sort` `Mathlib.Data.Finset.Density` `Mathlib.Data.Finset.MulAntidiagonal` `Mathlib.Data.Finset.NatDivisors` `Mathlib.Data.Finset.NoncommProd` `Mathlib.Data.Finset.SMulAntidiagonal` `Mathlib.Data.Finset.Slice` `Mathlib.Data.Finsupp.BigOperators` `Mathlib.Data.Finsupp.Fin` `Mathlib.Data.Finsupp.Fintype` `Mathlib.Data.Finsupp.Indicator` `Mathlib.Data.Finsupp.Notation` `Mathlib.Data.Finsupp.Pointwise` `Mathlib.Data.Finsupp.SMulWithZero` `Mathlib.Data.Finsupp.Single` `Mathlib.Data.Fintype.BigOperators` `Mathlib.Data.Fintype.CardEmbedding` `Mathlib.Data.Fintype.Fin` `Mathlib.Data.Holor` `Mathlib.Data.Int.Interval` `Mathlib.Data.Int.Log` `Mathlib.Data.Int.SuccPred` `Mathlib.Data.Int.WithZero` `Mathlib.Data.List.ToFinsupp` `Mathlib.Data.Matrix.Mul` `Mathlib.Data.Matrix.PEquiv` `Mathlib.Data.Multiset.Fintype` `Mathlib.Data.NNRat.BigOperators` `Mathlib.Data.NNRat.Floor` `Mathlib.Data.NNRat.Lemmas` `Mathlib.Data.NNRat.Order` `Mathlib.Data.NNReal.Basic` `Mathlib.Data.NNReal.Defs` `Mathlib.Data.Nat.Choose.Central` `Mathlib.Data.Nat.Choose.Sum` `Mathlib.Data.Nat.Digits` `Mathlib.Data.Nat.Factorial.BigOperators` `Mathlib.Data.Nat.Factorial.DoubleFactorial` `Mathlib.Data.Nat.Fib.Basic` `Mathlib.Data.Nat.Fib.Zeckendorf` `Mathlib.Data.Nat.Lattice` `Mathlib.Data.Nat.Multiplicity` `Mathlib.Data.Nat.PartENat` `Mathlib.Data.Nat.SuccPred` `Mathlib.Data.Ordmap.Ordset` `Mathlib.Data.PNat.Interval` `Mathlib.Data.Pi.Interval` `Mathlib.Data.Rat.Cast.Lemmas` `Mathlib.Data.Rat.Cast.Order` `Mathlib.Data.Rat.Floor` `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.Set.Equitable` `Mathlib.Data.Set.MulAntidiagonal` `Mathlib.Data.Set.Pointwise.Support` `Mathlib.Data.Set.SMulAntidiagonal` `Mathlib.Data.Sign` `Mathlib.Dynamics.BirkhoffSum.Average` `Mathlib.Dynamics.BirkhoffSum.Basic` `Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage` `Mathlib.GroupTheory.Perm.List` `Mathlib.GroupTheory.Perm.Support` `Mathlib.LinearAlgebra.Matrix.Orthogonal` `Mathlib.MeasureTheory.MeasurableSpace.Defs` `Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable` `Mathlib.MeasureTheory.MeasurableSpace.Instances` `Mathlib.MeasureTheory.MeasurableSpace.Invariants` `Mathlib.MeasureTheory.Measure.AddContent` `Mathlib.MeasureTheory.PiSystem` `Mathlib.MeasureTheory.SetAlgebra` `Mathlib.MeasureTheory.SetSemiring` `Mathlib.NumberTheory.ADEInequality` `Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue` `Mathlib.NumberTheory.Divisors` `Mathlib.NumberTheory.EllipticDivisibilitySequence` `Mathlib.NumberTheory.FactorisationProperties` `Mathlib.NumberTheory.Harmonic.Defs` `Mathlib.NumberTheory.Padics.PadicNorm` `Mathlib.NumberTheory.Padics.PadicVal.Basic` `Mathlib.NumberTheory.Padics.PadicVal.Defs` `Mathlib.Order.CompleteLatticeIntervals` `Mathlib.Order.Disjointed` `Mathlib.Order.Filter.AtTopBot.Archimedean` `Mathlib.Order.Filter.AtTopBot.BigOperators` `Mathlib.Order.Filter.AtTopBot.Floor` `Mathlib.Order.Filter.IndicatorFunction` `Mathlib.Order.Filter.Interval` `Mathlib.Order.Grade` `Mathlib.Order.Height` `Mathlib.Order.Interval.Finset.Basic` `Mathlib.Order.Interval.Finset.Box` `Mathlib.Order.Interval.Finset.Fin` `Mathlib.Order.Interval.Finset.Nat` `Mathlib.Order.Interval.Multiset` `Mathlib.Order.Interval.Set.Monotone` `Mathlib.Order.Interval.Set.OrdConnectedComponent` `Mathlib.Order.LiminfLimsup` `Mathlib.Order.OrderIsoNat` `Mathlib.Order.PartialSups` `Mathlib.Order.Restriction` `Mathlib.Order.SuccPred.Archimedean` `Mathlib.Order.SuccPred.Basic` `Mathlib.Order.SuccPred.CompleteLinearOrder` `Mathlib.Order.SuccPred.IntervalSucc` `Mathlib.Order.SuccPred.Limit` `Mathlib.Order.SuccPred.LinearLocallyFinite` `Mathlib.Order.SuccPred.Relation` `Mathlib.Order.SuccPred.WithBot` `Mathlib.Order.SupIndep` `Mathlib.Order.TransfiniteIteration` `Mathlib.Order.WellFoundedSet` `Mathlib.RingTheory.Coprime.Lemmas` `Mathlib.RingTheory.HahnSeries.Addition` `Mathlib.RingTheory.HahnSeries.Basic` `Mathlib.RingTheory.Multiplicity` `Mathlib.RingTheory.Nilpotent.Defs` `Mathlib.RingTheory.Prime` `Mathlib.Tactic.IntervalCases` `Mathlib.Tactic.Linarith` `Mathlib.Tactic.NormNum.BigOperators` `Mathlib.Tactic.NormNum.GCD` `Mathlib.Tactic.NormNum.IsCoprime` `Mathlib.Tactic.NormNum.NatFib` `Mathlib.Tactic.NormNum.NatSqrt` `Mathlib.Tactic.NormNum.OfScientific` `Mathlib.Tactic.NormNum` `Mathlib.Tactic.Positivity.Finset` `Mathlib.Tactic.Positivity` `Mathlib.Tactic.RewriteSearch` `Mathlib.Tactic.Rify` `Mathlib.Topology.Algebra.Indicator` `Mathlib.Topology.EMetricSpace.Defs` `Mathlib.Topology.MetricSpace.MetricSeparated` `Mathlib.Topology.Order.LeftRight` `Mathlib.Topology.PreorderRestrict` `Mathlib.Topology.UniformSpace.AbsoluteValue` `Mathlib.adomaniLeanUtils.importAutocomplete` `Mathlib.adomaniLeanUtils.importTryThis`	3
`Mathlib.Algebra.Order.CauSeq.Basic` `Mathlib.Algebra.Order.CauSeq.Completion`	6
4 files `Mathlib.Algebra.Order.Field.Basic` `Mathlib.Algebra.Order.Field.Power` `Mathlib.Data.Nat.Cast.Order.Field` `Mathlib.Order.Interval.Set.IsoIoo`	12
6 files `Mathlib.Algebra.Order.AbsoluteValue.Basic` `Mathlib.Algebra.Order.AbsoluteValue.Euclidean` `Mathlib.Algebra.Order.Hom.Basic` `Mathlib.Data.Int.AbsoluteValue` `Mathlib.Order.ModularLattice` `Mathlib.Tactic.Positivity.Basic`	13
12 files `Mathlib.Algebra.CharZero.Lemmas` `Mathlib.Algebra.Group.FiniteSupport` `Mathlib.Algebra.Group.Indicator` `Mathlib.Algebra.Group.Support` `Mathlib.Algebra.GroupWithZero.Indicator` `Mathlib.Algebra.Module.Basic` `Mathlib.Data.Finsupp.Defs` `Mathlib.Data.Finsupp.NeLocus` `Mathlib.Data.Int.CharZero` `Mathlib.Order.Cover` `Mathlib.Order.Interval.Set.OrdConnected` `Mathlib.Order.Interval.Set.ProjIcc`	14
`Mathlib.Order.Antichain`	15

b-mehta · 2025-01-27T17:51:45Z

Thanks for this! Interesting to see that this gives an import difference of 15 rather than the import difference of 14 reported by the bot earlier - I suppose this is because of other changes that got merged at the same time?

adomani · 2025-01-27T18:01:54Z

I do not know where the "extra" import comes from, but I did have to pick manually a reference commit and I chose HEAD~ to try and avoid further contamination. The bot uses the "latest branching from master", but I was not really able to do that easily in the detached head.

add lemmas relating chains to antichains

b53ec42

b-mehta added the t-order Order theory label Jan 14, 2025

b-mehta mentioned this pull request Jan 14, 2025

[Merged by Bors] - feat(Counterexamples): disproof of the Aharoni–Korman conjecture #20082

Closed

8 tasks

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Jan 14, 2025

b-mehta requested a review from YaelDillies January 16, 2025 22:49

vihdzp reviewed Jan 17, 2025

View reviewed changes

Mathlib/Order/Antichain.lean Show resolved Hide resolved

Mathlib/Order/Antichain.lean Outdated Show resolved Hide resolved

golf?

21693f4

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 22, 2025

ghost added the ready-to-merge This PR has been sent to bors. label Jan 23, 2025

mathlib-bors bot changed the title ~~feat(Order): relate chains to antichains~~ [Merged by Bors] - feat(Order): relate chains to antichains Jan 23, 2025

mathlib-bors bot closed this Jan 23, 2025

mathlib-bors bot deleted the chain-antichain branch January 23, 2025 07:41

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(Order): relate chains to antichains#20756

[Merged by Bors] - feat(Order): relate chains to antichains#20756
b-mehta wants to merge 2 commits intomasterfrom
chain-antichain

b-mehta commented Jan 14, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Jan 14, 2025 •

edited

Loading

Uh oh!

vihdzp left a comment

Uh oh!

Uh oh!

Uh oh!

YaelDillies commented Jan 17, 2025

Uh oh!

YaelDillies commented Jan 22, 2025

Uh oh!

github-actions bot commented Jan 22, 2025

Uh oh!

jcommelin commented Jan 23, 2025

Uh oh!

mathlib-bors bot commented Jan 23, 2025

Uh oh!

mathlib-bors bot commented Jan 23, 2025

Uh oh!

adomani commented Jan 27, 2025

Uh oh!

b-mehta commented Jan 27, 2025

Uh oh!

adomani commented Jan 27, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Conversation

b-mehta commented Jan 14, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

vihdzp left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

YaelDillies commented Jan 17, 2025

Uh oh!

YaelDillies commented Jan 22, 2025

Uh oh!

github-actions bot commented Jan 22, 2025

Uh oh!

jcommelin commented Jan 23, 2025

Uh oh!

mathlib-bors bot commented Jan 23, 2025

Uh oh!

mathlib-bors bot commented Jan 23, 2025

Uh oh!

adomani commented Jan 27, 2025

Import changes for all files

Uh oh!

b-mehta commented Jan 27, 2025

Uh oh!

adomani commented Jan 27, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

b-mehta commented Jan 14, 2025 •

edited

Loading

github-actions bot commented Jan 14, 2025 •

edited

Loading