[Merged by Bors] - feat(Algebra/Order/Floor): `⌊n * x⌋₊ / n = ⌊x⌋₊` by vasnesterov · Pull Request #26004 · leanprover-community/mathlib4

vasnesterov · 2025-06-17T08:05:40Z

Prove that ⌊n * x⌋₊ / n = ⌊x⌋₊ for natural n.

github-actions · 2025-06-17T08:07:03Z

PR summary 7260822b74

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Order.Floor.Semiring	623	622	-1 (-0.16%)

Import changes for all files

Files	Import difference
721 files `Mathlib.Algebra.AddConstMap.Basic` `Mathlib.Algebra.AddConstMap.Equiv` `Mathlib.Algebra.Category.ContinuousCohomology.Basic` `Mathlib.Algebra.Category.Grp.EnoughInjectives` `Mathlib.Algebra.Category.Grp.Injective` `Mathlib.Algebra.Category.Grp.LargeColimits` `Mathlib.Algebra.Category.Grp.Ulift` `Mathlib.Algebra.Category.ModuleCat.Differentials.Basic` `Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf` `Mathlib.Algebra.Category.ModuleCat.EnoughInjectives` `Mathlib.Algebra.Category.ModuleCat.Topology.Basic` `Mathlib.Algebra.Category.ModuleCat.Topology.Homology` `Mathlib.Algebra.Category.Ring.LinearAlgebra` `Mathlib.Algebra.Category.Ring.Under.Limits` `Mathlib.Algebra.Central.TensorProduct` `Mathlib.Algebra.CharP.LinearMaps` `Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries` `Mathlib.Algebra.Field.Periodic` `Mathlib.Algebra.Lie.CartanExists` `Mathlib.Algebra.Lie.CartanSubalgebra` `Mathlib.Algebra.Lie.Character` `Mathlib.Algebra.Lie.Derivation.Killing` `Mathlib.Algebra.Lie.EngelSubalgebra` `Mathlib.Algebra.Lie.Engel` `Mathlib.Algebra.Lie.InvariantForm` `Mathlib.Algebra.Lie.Killing` `Mathlib.Algebra.Lie.LieTheorem` `Mathlib.Algebra.Lie.Nilpotent` `Mathlib.Algebra.Lie.Rank` `Mathlib.Algebra.Lie.Semisimple.Basic` `Mathlib.Algebra.Lie.Semisimple.Defs` `Mathlib.Algebra.Lie.Semisimple.Lemmas` `Mathlib.Algebra.Lie.Solvable` `Mathlib.Algebra.Lie.TraceForm` `Mathlib.Algebra.Lie.Weights.Basic` `Mathlib.Algebra.Lie.Weights.Cartan` `Mathlib.Algebra.Lie.Weights.Chain` `Mathlib.Algebra.Lie.Weights.Killing` `Mathlib.Algebra.Lie.Weights.Linear` `Mathlib.Algebra.Lie.Weights.RootSystem` `Mathlib.Algebra.Module.CharacterModule` `Mathlib.Algebra.Module.DedekindDomain` `Mathlib.Algebra.Module.PID` `Mathlib.Algebra.Module.Presentation.Differentials` `Mathlib.Algebra.Module.Torsion` `Mathlib.Algebra.Module.ZMod` `Mathlib.Algebra.Order.Archimedean.Basic` `Mathlib.Algebra.Order.Archimedean.Class` `Mathlib.Algebra.Order.Archimedean.Hom` `Mathlib.Algebra.Order.Archimedean.IndicatorCard` `Mathlib.Algebra.Order.Archimedean.Submonoid` `Mathlib.Algebra.Order.CauSeq.BigOperators` `Mathlib.Algebra.Order.CompleteField` `Mathlib.Algebra.Order.Floor.Semiring` `Mathlib.Algebra.Order.Floor` `Mathlib.Algebra.Order.ToIntervalMod` `Mathlib.Algebra.Polynomial.Module.FiniteDimensional` `Mathlib.Algebra.Star.CHSH` `Mathlib.AlgebraicGeometry.AffineScheme` `Mathlib.AlgebraicGeometry.AffineSpace` `Mathlib.AlgebraicGeometry.AffineTransitionLimit` `Mathlib.AlgebraicGeometry.Cover.Over` `Mathlib.AlgebraicGeometry.Cover.Sigma` `Mathlib.AlgebraicGeometry.Fiber` `Mathlib.AlgebraicGeometry.FunctionField` `Mathlib.AlgebraicGeometry.GluingOneHypercover` `Mathlib.AlgebraicGeometry.IdealSheaf.Basic` `Mathlib.AlgebraicGeometry.IdealSheaf.Functorial` `Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme` `Mathlib.AlgebraicGeometry.IdealSheaf` `Mathlib.AlgebraicGeometry.Limits` `Mathlib.AlgebraicGeometry.Morphisms.AffineAnd` `Mathlib.AlgebraicGeometry.Morphisms.Affine` `Mathlib.AlgebraicGeometry.Morphisms.Basic` `Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Constructors` `Mathlib.AlgebraicGeometry.Morphisms.Etale` `Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation` `Mathlib.AlgebraicGeometry.Morphisms.FiniteType` `Mathlib.AlgebraicGeometry.Morphisms.Finite` `Mathlib.AlgebraicGeometry.Morphisms.Flat` `Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified` `Mathlib.AlgebraicGeometry.Morphisms.Immersion` `Mathlib.AlgebraicGeometry.Morphisms.Integral` `Mathlib.AlgebraicGeometry.Morphisms.IsIso` `Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Preimmersion` `Mathlib.AlgebraicGeometry.Morphisms.Proper` `Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact` `Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated` `Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties` `Mathlib.AlgebraicGeometry.Morphisms.Separated` `Mathlib.AlgebraicGeometry.Morphisms.Smooth` `Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks` `Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen` `Mathlib.AlgebraicGeometry.Noetherian` `Mathlib.AlgebraicGeometry.PointsPi` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper` `Mathlib.AlgebraicGeometry.Properties` `Mathlib.AlgebraicGeometry.PullbackCarrier` `Mathlib.AlgebraicGeometry.Pullbacks` `Mathlib.AlgebraicGeometry.RationalMap` `Mathlib.AlgebraicGeometry.ResidueField` `Mathlib.AlgebraicGeometry.Sites.BigZariski` `Mathlib.AlgebraicGeometry.Sites.Etale` `Mathlib.AlgebraicGeometry.Sites.MorphismProperty` `Mathlib.AlgebraicGeometry.Sites.Representability` `Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski` `Mathlib.AlgebraicGeometry.Sites.Small` `Mathlib.AlgebraicGeometry.SpreadingOut` `Mathlib.AlgebraicGeometry.Stalk` `Mathlib.AlgebraicGeometry.ValuativeCriterion` `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.SingularHomology.Basic` `Mathlib.AlgebraicTopology.SingularSet` `Mathlib.AlgebraicTopology.TopologicalSimplex` `Mathlib.Analysis.Asymptotics.AsymptoticEquivalent` `Mathlib.Analysis.Asymptotics.Completion` `Mathlib.Analysis.Asymptotics.Defs` `Mathlib.Analysis.Asymptotics.Lemmas` `Mathlib.Analysis.Asymptotics.SuperpolynomialDecay` `Mathlib.Analysis.Asymptotics.TVS` `Mathlib.Analysis.Asymptotics.Theta` `Mathlib.Analysis.BoxIntegral.Box.Basic` `Mathlib.Analysis.BoxIntegral.Partition.Additive` `Mathlib.Analysis.BoxIntegral.Partition.Basic` `Mathlib.Analysis.BoxIntegral.Partition.Split` `Mathlib.Analysis.BoxIntegral.Partition.Tagged` `Mathlib.Analysis.CStarAlgebra.Basic` `Mathlib.Analysis.CStarAlgebra.Classes` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary` `Mathlib.Analysis.CStarAlgebra.ContinuousMap` `Mathlib.Analysis.CStarAlgebra.Module.Synonym` `Mathlib.Analysis.CStarAlgebra.Unitization` `Mathlib.Analysis.Calculus.FDeriv.Defs` `Mathlib.Analysis.Calculus.FormalMultilinearSeries` `Mathlib.Analysis.Complex.Asymptotics` `Mathlib.Analysis.Complex.Basic` `Mathlib.Analysis.Complex.Convex` `Mathlib.Analysis.Complex.IntegerCompl` `Mathlib.Analysis.Complex.IsIntegral` `Mathlib.Analysis.Complex.OperatorNorm` `Mathlib.Analysis.Complex.ReImTopology` `Mathlib.Analysis.Complex.UpperHalfPlane.Basic` `Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty` `Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction` `Mathlib.Analysis.Complex.UpperHalfPlane.Topology` `Mathlib.Analysis.ConstantSpeed` `Mathlib.Analysis.Convex.Cone.Basic` `Mathlib.Analysis.Convex.Cone.Extension` `Mathlib.Analysis.Convex.Contractible` `Mathlib.Analysis.Convex.EGauge` `Mathlib.Analysis.Convex.Exposed` `Mathlib.Analysis.Convex.Extrema` `Mathlib.Analysis.Convex.PathConnected` `Mathlib.Analysis.Convex.Strict` `Mathlib.Analysis.Convex.Strong` `Mathlib.Analysis.Convex.Topology` `Mathlib.Analysis.Convex.TotallyBounded` `Mathlib.Analysis.Convex.Visible` `Mathlib.Analysis.InnerProductSpace.Affine` `Mathlib.Analysis.InnerProductSpace.Basic` `Mathlib.Analysis.InnerProductSpace.Defs` `Mathlib.Analysis.LocallyConvex.AbsConvex` `Mathlib.Analysis.LocallyConvex.BalancedCoreHull` `Mathlib.Analysis.LocallyConvex.Barrelled` `Mathlib.Analysis.LocallyConvex.Basic` `Mathlib.Analysis.LocallyConvex.Bounded` `Mathlib.Analysis.LocallyConvex.ContinuousOfBounded` `Mathlib.Analysis.LocallyConvex.Polar` `Mathlib.Analysis.LocallyConvex.StrongTopology` `Mathlib.Analysis.LocallyConvex.WeakDual` `Mathlib.Analysis.LocallyConvex.WithSeminorms` `Mathlib.Analysis.Normed.Affine.AddTorsor` `Mathlib.Analysis.Normed.Affine.ContinuousAffineMap` `Mathlib.Analysis.Normed.Affine.Isometry` `Mathlib.Analysis.Normed.Affine.MazurUlam` `Mathlib.Analysis.Normed.Affine.Simplex` `Mathlib.Analysis.Normed.Algebra.Ultra` `Mathlib.Analysis.Normed.Algebra.Unitization` `Mathlib.Analysis.Normed.Field.Basic` `Mathlib.Analysis.Normed.Field.Instances` `Mathlib.Analysis.Normed.Field.Lemmas` `Mathlib.Analysis.Normed.Field.Ultra` `Mathlib.Analysis.Normed.Field.UnitBall` `Mathlib.Analysis.Normed.Field.WithAbs` `Mathlib.Analysis.Normed.Group.AddTorsor` `Mathlib.Analysis.Normed.Group.BallSphere` `Mathlib.Analysis.Normed.Group.Basic` `Mathlib.Analysis.Normed.Group.Bounded` `Mathlib.Analysis.Normed.Group.CocompactMap` `Mathlib.Analysis.Normed.Group.Completion` `Mathlib.Analysis.Normed.Group.Constructions` `Mathlib.Analysis.Normed.Group.Continuity` `Mathlib.Analysis.Normed.Group.HomCompletion` `Mathlib.Analysis.Normed.Group.Hom` `Mathlib.Analysis.Normed.Group.InfiniteSum` `Mathlib.Analysis.Normed.Group.Int` `Mathlib.Analysis.Normed.Group.Lemmas` `Mathlib.Analysis.Normed.Group.NullSubmodule` `Mathlib.Analysis.Normed.Group.Rat` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion` `Mathlib.Analysis.Normed.Group.SemiNormedGrp` `Mathlib.Analysis.Normed.Group.Seminorm` `Mathlib.Analysis.Normed.Group.SeparationQuotient` `Mathlib.Analysis.Normed.Group.Subgroup` `Mathlib.Analysis.Normed.Group.Submodule` `Mathlib.Analysis.Normed.Group.Tannery` `Mathlib.Analysis.Normed.Group.Ultra` `Mathlib.Analysis.Normed.Group.Uniform` `Mathlib.Analysis.Normed.Group.ZeroAtInfty` `Mathlib.Analysis.Normed.Lp.WithLp` `Mathlib.Analysis.Normed.Module.Basic` `Mathlib.Analysis.Normed.Module.Completion` `Mathlib.Analysis.Normed.Module.Ray` `Mathlib.Analysis.Normed.Module.Span` `Mathlib.Analysis.Normed.MulAction` `Mathlib.Analysis.Normed.Operator.Compact` `Mathlib.Analysis.Normed.Operator.ContinuousLinearMap` `Mathlib.Analysis.Normed.Operator.LinearIsometry` `Mathlib.Analysis.Normed.Order.Basic` `Mathlib.Analysis.Normed.Order.Hom.Basic` `Mathlib.Analysis.Normed.Order.Hom.Ultra` `Mathlib.Analysis.Normed.Order.Lattice` `Mathlib.Analysis.Normed.Ring.Basic` `Mathlib.Analysis.Normed.Ring.InfiniteSum` `Mathlib.Analysis.Normed.Ring.Lemmas` `Mathlib.Analysis.Normed.Ring.Ultra` `Mathlib.Analysis.Normed.Ring.WithAbs` `Mathlib.Analysis.NormedSpace.Alternating.Basic` `Mathlib.Analysis.NormedSpace.Alternating.Curry` `Mathlib.Analysis.NormedSpace.BallAction` `Mathlib.Analysis.NormedSpace.ConformalLinearMap` `Mathlib.Analysis.NormedSpace.ENormedSpace` `Mathlib.Analysis.NormedSpace.Extend` `Mathlib.Analysis.NormedSpace.Extr` `Mathlib.Analysis.NormedSpace.FunctionSeries` `Mathlib.Analysis.NormedSpace.IndicatorFunction` `Mathlib.Analysis.NormedSpace.Int` `Mathlib.Analysis.NormedSpace.MStructure` `Mathlib.Analysis.NormedSpace.Multilinear.Basic` `Mathlib.Analysis.NormedSpace.Multilinear.Curry` `Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics` `Mathlib.Analysis.NormedSpace.OperatorNorm.Basic` `Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear` `Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness` `Mathlib.Analysis.NormedSpace.OperatorNorm.Mul` `Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm` `Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace` `Mathlib.Analysis.NormedSpace.OperatorNorm.Prod` `Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm` `Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm` `Mathlib.Analysis.NormedSpace.Real` `Mathlib.Analysis.NormedSpace.SphereNormEquiv` `Mathlib.Analysis.Oscillation` `Mathlib.Analysis.Polynomial.CauchyBound` `Mathlib.Analysis.RCLike.Basic` `Mathlib.Analysis.RCLike.BoundedContinuous` `Mathlib.Analysis.Seminorm` `Mathlib.Analysis.SpecialFunctions.Log.ERealExp` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev` `Mathlib.Analysis.Subadditive` `Mathlib.Analysis.SumOverResidueClass` `Mathlib.CategoryTheory.Galois.Equivalence` `Mathlib.CategoryTheory.Galois.EssSurj` `Mathlib.CategoryTheory.Galois.IsFundamentalgroup` `Mathlib.CategoryTheory.Galois.Topology` `Mathlib.Combinatorics.Schnirelmann` `Mathlib.Combinatorics.SimpleGraph.Extremal.Basic` `Mathlib.Data.Complex.Exponential` `Mathlib.Data.Complex.Norm` `Mathlib.Data.Complex.Order` `Mathlib.Data.Complex.Trigonometric` `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.EReal.Basic` `Mathlib.Data.EReal.Operations` `Mathlib.Data.Int.Log` `Mathlib.Data.Int.WithZero` `Mathlib.Data.NNRat.Floor` `Mathlib.Data.NNReal.Basic` `Mathlib.Data.NNReal.Defs` `Mathlib.Data.NNReal.Star` `Mathlib.Data.Real.Archimedean` `Mathlib.Data.Real.CompleteField` `Mathlib.Data.Real.ConjExponents` `Mathlib.Data.Real.ENatENNReal` `Mathlib.Data.Real.EReal` `Mathlib.Data.Real.GoldenRatio` `Mathlib.Data.Real.Irrational` `Mathlib.Data.Real.Pointwise` `Mathlib.Data.Real.Sqrt` `Mathlib.Data.Real.StarOrdered` `Mathlib.Dynamics.BirkhoffSum.NormedSpace` `Mathlib.FieldTheory.AbsoluteGaloisGroup` `Mathlib.FieldTheory.Galois.Infinite` `Mathlib.FieldTheory.JacobsonNoether` `Mathlib.FieldTheory.KrullTopology` `Mathlib.FieldTheory.Laurent` `Mathlib.FieldTheory.LinearDisjoint` `Mathlib.FieldTheory.PurelyInseparable.Tower` `Mathlib.FieldTheory.RatFunc.AsPolynomial` `Mathlib.FieldTheory.RatFunc.Degree` `Mathlib.Geometry.Euclidean.Inversion.Basic` `Mathlib.Geometry.Manifold.ChartedSpace` `Mathlib.Geometry.Manifold.LocalInvariantProperties` `Mathlib.Geometry.Manifold.Sheaf.Basic` `Mathlib.GroupTheory.ArchimedeanDensely` `Mathlib.GroupTheory.Archimedean` `Mathlib.GroupTheory.FiniteAbelian.Basic` `Mathlib.GroupTheory.FiniteAbelian.Duality` `Mathlib.GroupTheory.Frattini` `Mathlib.GroupTheory.Nilpotent` `Mathlib.GroupTheory.RegularWreathProduct` `Mathlib.GroupTheory.Schreier` `Mathlib.GroupTheory.SchurZassenhaus` `Mathlib.GroupTheory.SpecificGroups.ZGroup` `Mathlib.GroupTheory.Sylow` `Mathlib.GroupTheory.Transfer` `Mathlib.InformationTheory.Hamming` `Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv` `Mathlib.LinearAlgebra.Dimension.Torsion.Basic` `Mathlib.LinearAlgebra.Dimension.Torsion.Finite` `Mathlib.LinearAlgebra.Eigenspace.Semisimple` `Mathlib.LinearAlgebra.Eigenspace.Zero` `Mathlib.LinearAlgebra.FreeModule.ModN` `Mathlib.LinearAlgebra.JordanChevalley` `Mathlib.LinearAlgebra.LinearDisjoint` `Mathlib.LinearAlgebra.Matrix.Gershgorin` `Mathlib.LinearAlgebra.QuadraticForm.Real` `Mathlib.LinearAlgebra.Reflection` `Mathlib.LinearAlgebra.RootSystem.BaseChange` `Mathlib.LinearAlgebra.RootSystem.Base` `Mathlib.LinearAlgebra.RootSystem.Basic` `Mathlib.LinearAlgebra.RootSystem.CartanMatrix` `Mathlib.LinearAlgebra.RootSystem.Chain` `Mathlib.LinearAlgebra.RootSystem.Defs` `Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear` `Mathlib.LinearAlgebra.RootSystem.Finite.G2` `Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas` `Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction` `Mathlib.LinearAlgebra.RootSystem.Hom` `Mathlib.LinearAlgebra.RootSystem.Irreducible` `Mathlib.LinearAlgebra.RootSystem.IsValuedIn` `Mathlib.LinearAlgebra.RootSystem.OfBilinear` `Mathlib.LinearAlgebra.RootSystem.Reduced` `Mathlib.LinearAlgebra.RootSystem.RootPairingCat` `Mathlib.LinearAlgebra.RootSystem.RootPositive` `Mathlib.LinearAlgebra.RootSystem.WeylGroup` `Mathlib.LinearAlgebra.Semisimple` `Mathlib.MeasureTheory.OuterMeasure.AE` `Mathlib.MeasureTheory.OuterMeasure.Basic` `Mathlib.MeasureTheory.OuterMeasure.BorelCantelli` `Mathlib.MeasureTheory.OuterMeasure.Defs` `Mathlib.MeasureTheory.OuterMeasure.Operations` `Mathlib.ModelTheory.Fraisse` `Mathlib.ModelTheory.Order` `Mathlib.NumberTheory.ClassNumber.AdmissibleAbs` `Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter` `Mathlib.NumberTheory.DiophantineApproximation.Basic` `Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions` `Mathlib.NumberTheory.DirichletCharacter.Bounds` `Mathlib.NumberTheory.DirichletCharacter.Orthogonality` `Mathlib.NumberTheory.FermatPsp` `Mathlib.NumberTheory.FunctionField` `Mathlib.NumberTheory.Harmonic.Int` `Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs` `Mathlib.NumberTheory.ModularForms.Identities` `Mathlib.NumberTheory.ModularForms.SlashActions` `Mathlib.NumberTheory.ModularForms.SlashInvariantForms` `Mathlib.NumberTheory.Modular` `Mathlib.NumberTheory.MulChar.Duality` `Mathlib.NumberTheory.NumberField.Discriminant.Defs` `Mathlib.NumberTheory.NumberField.Discriminant.Different` `Mathlib.NumberTheory.NumberField.FractionalIdeal` `Mathlib.NumberTheory.Padics.PadicIntegers` `Mathlib.NumberTheory.Padics.PadicNumbers` `Mathlib.NumberTheory.Padics.RingHoms` `Mathlib.NumberTheory.Pell` `Mathlib.NumberTheory.RamificationInertia.Basic` `Mathlib.NumberTheory.RamificationInertia.Galois` `Mathlib.NumberTheory.RamificationInertia.Unramified` `Mathlib.NumberTheory.Rayleigh` `Mathlib.NumberTheory.SelbergSieve` `Mathlib.NumberTheory.SumTwoSquares` `Mathlib.NumberTheory.Zsqrtd.GaussianInt` `Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity` `Mathlib.NumberTheory.Zsqrtd.ToReal` `Mathlib.Order.Filter.AtTopBot.Archimedean` `Mathlib.Order.Filter.AtTopBot.Floor` `Mathlib.Order.Filter.ENNReal` `Mathlib.Order.Filter.ZeroAndBoundedAtFilter` `Mathlib.RingTheory.AdicCompletion.Algebra` `Mathlib.RingTheory.AdicCompletion.AsTensorProduct` `Mathlib.RingTheory.AdicCompletion.Exactness` `Mathlib.RingTheory.AdicCompletion.Functoriality` `Mathlib.RingTheory.CotangentLocalizationAway` `Mathlib.RingTheory.DedekindDomain.AdicValuation` `Mathlib.RingTheory.DedekindDomain.Different` `Mathlib.RingTheory.DedekindDomain.Dvr` `Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing` `Mathlib.RingTheory.DedekindDomain.PID` `Mathlib.RingTheory.DedekindDomain.SInteger` `Mathlib.RingTheory.DedekindDomain.SelmerGroup` `Mathlib.RingTheory.DiscreteValuationRing.TFAE` `Mathlib.RingTheory.Etale.Basic` `Mathlib.RingTheory.Etale.Field` `Mathlib.RingTheory.Etale.Kaehler` `Mathlib.RingTheory.Etale.Pi` `Mathlib.RingTheory.Extension.Basic` `Mathlib.RingTheory.Extension.Cotangent.Basic` `Mathlib.RingTheory.Extension.Cotangent.LocalizationAway` `Mathlib.RingTheory.Extension.Generators` `Mathlib.RingTheory.Extension.Presentation.Basic` `Mathlib.RingTheory.Extension` `Mathlib.RingTheory.Flat.Basic` `Mathlib.RingTheory.Flat.CategoryTheory` `Mathlib.RingTheory.Flat.Domain` `Mathlib.RingTheory.Flat.Equalizer` `Mathlib.RingTheory.Flat.EquationalCriterion` `Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra` `Mathlib.RingTheory.Flat.FaithfullyFlat.Basic` `Mathlib.RingTheory.Flat.Localization` `Mathlib.RingTheory.Flat.Stability` `Mathlib.RingTheory.FractionalIdeal.Norm` `Mathlib.RingTheory.Frobenius` `Mathlib.RingTheory.Generators` `Mathlib.RingTheory.HopkinsLevitzki` `Mathlib.RingTheory.Ideal.Cotangent` `Mathlib.RingTheory.Ideal.GoingDown` `Mathlib.RingTheory.Ideal.Int` `Mathlib.RingTheory.Ideal.KrullsHeightTheorem` `Mathlib.RingTheory.Ideal.Norm.AbsNorm` `Mathlib.RingTheory.Ideal.Norm.RelNorm` `Mathlib.RingTheory.Jacobson.Artinian` `Mathlib.RingTheory.Kaehler.Basic` `Mathlib.RingTheory.Kaehler.CotangentComplex` `Mathlib.RingTheory.Kaehler.JacobiZariski` `Mathlib.RingTheory.Kaehler.Polynomial` `Mathlib.RingTheory.Kaehler.TensorProduct` `Mathlib.RingTheory.LaurentSeries` `Mathlib.RingTheory.LinearDisjoint` `Mathlib.RingTheory.LocalRing.Module` `Mathlib.RingTheory.MvPowerSeries.Evaluation` `Mathlib.RingTheory.MvPowerSeries.LinearTopology` `Mathlib.RingTheory.MvPowerSeries.PiTopology` `Mathlib.RingTheory.MvPowerSeries.Substitution` `Mathlib.RingTheory.OrderOfVanishing` `Mathlib.RingTheory.Polynomial.GaussNorm` `Mathlib.RingTheory.PowerSeries.Evaluation` `Mathlib.RingTheory.PowerSeries.GaussNorm` `Mathlib.RingTheory.PowerSeries.PiTopology` `Mathlib.RingTheory.PowerSeries.Substitution` `Mathlib.RingTheory.Presentation` `Mathlib.RingTheory.Regular.Depth` `Mathlib.RingTheory.Regular.IsSMulRegular` `Mathlib.RingTheory.Regular.RegularSequence` `Mathlib.RingTheory.RingHom.Flat` `Mathlib.RingTheory.RingHom.Smooth` `Mathlib.RingTheory.RingHom.StandardSmooth` `Mathlib.RingTheory.RingHom.Unramified` `Mathlib.RingTheory.Smooth.Basic` `Mathlib.RingTheory.Smooth.Kaehler` `Mathlib.RingTheory.Smooth.Local` `Mathlib.RingTheory.Smooth.Locus` `Mathlib.RingTheory.Smooth.Pi` `Mathlib.RingTheory.Smooth.StandardSmoothCotangent` `Mathlib.RingTheory.Smooth.StandardSmooth` `Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity` `Mathlib.RingTheory.Spectrum.Prime.Chevalley` `Mathlib.RingTheory.Spectrum.Prime.FreeLocus` `Mathlib.RingTheory.Spectrum.Prime.Homeomorph` `Mathlib.RingTheory.Spectrum.Prime.LTSeries` `Mathlib.RingTheory.Spectrum.Prime.Polynomial` `Mathlib.RingTheory.TensorProduct.Nontrivial` `Mathlib.RingTheory.Trace.Quotient` `Mathlib.RingTheory.Unramified.Basic` `Mathlib.RingTheory.Unramified.Field` `Mathlib.RingTheory.Unramified.Finite` `Mathlib.RingTheory.Unramified.LocalRing` `Mathlib.RingTheory.Unramified.Locus` `Mathlib.RingTheory.Unramified.Pi` `Mathlib.RingTheory.Valuation.Archimedean` `Mathlib.RingTheory.Valuation.RankOne` `Mathlib.RingTheory.WittVector.Compare` `Mathlib.Tactic.NormNum.RealSqrt` `Mathlib.Topology.Algebra.AffineSubspace` `Mathlib.Topology.Algebra.Algebra.Equiv` `Mathlib.Topology.Algebra.Algebra` `Mathlib.Topology.Algebra.ClopenNhdofOne` `Mathlib.Topology.Algebra.ClosedSubgroup` `Mathlib.Topology.Algebra.ContinuousAffineMap` `Mathlib.Topology.Algebra.Equicontinuity` `Mathlib.Topology.Algebra.Field` `Mathlib.Topology.Algebra.FilterBasis` `Mathlib.Topology.Algebra.Group.Basic` `Mathlib.Topology.Algebra.Group.ClosedSubgroup` `Mathlib.Topology.Algebra.Group.CompactOpen` `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.Group.TopologicalAbelianization` `Mathlib.Topology.Algebra.GroupCompletion` `Mathlib.Topology.Algebra.InfiniteSum.Constructions` `Mathlib.Topology.Algebra.InfiniteSum.ENNReal` `Mathlib.Topology.Algebra.InfiniteSum.Field` `Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion` `Mathlib.Topology.Algebra.InfiniteSum.Group` `Mathlib.Topology.Algebra.InfiniteSum.Module` `Mathlib.Topology.Algebra.InfiniteSum.NatInt` `Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean` `Mathlib.Topology.Algebra.InfiniteSum.Order` `Mathlib.Topology.Algebra.InfiniteSum.Real` `Mathlib.Topology.Algebra.InfiniteSum.Ring` `Mathlib.Topology.Algebra.InfiniteSum.UniformOn` `Mathlib.Topology.Algebra.IntermediateField` `Mathlib.Topology.Algebra.IsOpenUnits` `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.Alternating.Basic` `Mathlib.Topology.Algebra.Module.Alternating.Topology` `Mathlib.Topology.Algebra.Module.Basic` `Mathlib.Topology.Algebra.Module.CharacterSpace` `Mathlib.Topology.Algebra.Module.ClosedSubmodule` `Mathlib.Topology.Algebra.Module.Compact` `Mathlib.Topology.Algebra.Module.Determinant` `Mathlib.Topology.Algebra.Module.Equiv` `Mathlib.Topology.Algebra.Module.FiniteDimension` `Mathlib.Topology.Algebra.Module.LinearMapPiProd` `Mathlib.Topology.Algebra.Module.LinearMap` `Mathlib.Topology.Algebra.Module.LinearPMap` `Mathlib.Topology.Algebra.Module.LocallyConvex` `Mathlib.Topology.Algebra.Module.ModuleTopology` `Mathlib.Topology.Algebra.Module.Multilinear.Basic` `Mathlib.Topology.Algebra.Module.Multilinear.Bounded` `Mathlib.Topology.Algebra.Module.Multilinear.Topology` `Mathlib.Topology.Algebra.Module.PerfectPairing` `Mathlib.Topology.Algebra.Module.Simple` `Mathlib.Topology.Algebra.Module.Star` `Mathlib.Topology.Algebra.Module.StrongTopology` `Mathlib.Topology.Algebra.Module.UniformConvergence` `Mathlib.Topology.Algebra.Module.WeakBilin` `Mathlib.Topology.Algebra.Module.WeakDual` `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.LiminfLimsup` `Mathlib.Topology.Algebra.Order.UpperLower` `Mathlib.Topology.Algebra.Polynomial` `Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace` `Mathlib.Topology.Algebra.RestrictedProduct` `Mathlib.Topology.Algebra.Ring.Basic` `Mathlib.Topology.Algebra.Ring.Compact` `Mathlib.Topology.Algebra.Ring.Ideal` `Mathlib.Topology.Algebra.Ring.Real` `Mathlib.Topology.Algebra.SeparationQuotient.Basic` `Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional` `Mathlib.Topology.Algebra.SeparationQuotient.Hom` `Mathlib.Topology.Algebra.SeparationQuotient.Section` `Mathlib.Topology.Algebra.Star.Real` `Mathlib.Topology.Algebra.StarSubalgebra` `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.Valued.NormedValued` `Mathlib.Topology.Algebra.Valued.ValuationTopology` `Mathlib.Topology.Algebra.Valued.ValuedField` `Mathlib.Topology.Algebra.Valued.WithVal` `Mathlib.Topology.Bornology.BoundedOperation` `Mathlib.Topology.Bornology.Real` `Mathlib.Topology.CWComplex.Classical.Basic` `Mathlib.Topology.CWComplex.Classical.Finite` `Mathlib.Topology.Category.DeltaGenerated` `Mathlib.Topology.Category.TopCommRingCat` `Mathlib.Topology.Compactness.DeltaGeneratedSpace` `Mathlib.Topology.Compactness.PseudometrizableLindelof` `Mathlib.Topology.Connected.LocPathConnected` `Mathlib.Topology.Connected.PathComponentOne` `Mathlib.Topology.Connected.PathConnected` `Mathlib.Topology.ContinuousMap.Algebra` `Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli` `Mathlib.Topology.ContinuousMap.Bounded.Basic` `Mathlib.Topology.ContinuousMap.Bounded.Normed` `Mathlib.Topology.ContinuousMap.Bounded.Star` `Mathlib.Topology.ContinuousMap.BoundedCompactlySupported` `Mathlib.Topology.ContinuousMap.Compact` `Mathlib.Topology.ContinuousMap.CompactlySupported` `Mathlib.Topology.ContinuousMap.ContinuousMapZero` `Mathlib.Topology.ContinuousMap.ContinuousSqrt` `Mathlib.Topology.ContinuousMap.Lattice` `Mathlib.Topology.ContinuousMap.LocallyConstant` `Mathlib.Topology.ContinuousMap.LocallyConvex` `Mathlib.Topology.ContinuousMap.Periodic` `Mathlib.Topology.ContinuousMap.Polynomial` `Mathlib.Topology.ContinuousMap.StarOrdered` `Mathlib.Topology.ContinuousMap.Star` `Mathlib.Topology.ContinuousMap.ZeroAtInfty` `Mathlib.Topology.EMetricSpace.Basic` `Mathlib.Topology.EMetricSpace.BoundedVariation` `Mathlib.Topology.EMetricSpace.Defs` `Mathlib.Topology.EMetricSpace.Diam` `Mathlib.Topology.EMetricSpace.Lipschitz` `Mathlib.Topology.EMetricSpace.Paracompact` `Mathlib.Topology.EMetricSpace.Pi` `Mathlib.Topology.Germ` `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.AddCircle.Defs` `Mathlib.Topology.Instances.AddCircle.DenseSubgroup` `Mathlib.Topology.Instances.AddCircle.Real` `Mathlib.Topology.Instances.CantorSet` `Mathlib.Topology.Instances.ENNReal.Lemmas` `Mathlib.Topology.Instances.Int` `Mathlib.Topology.Instances.Irrational` `Mathlib.Topology.Instances.Matrix` `Mathlib.Topology.Instances.NNReal.Lemmas` `Mathlib.Topology.Instances.Nat` `Mathlib.Topology.Instances.PNat` `Mathlib.Topology.Instances.RatLemmas` `Mathlib.Topology.Instances.Rat` `Mathlib.Topology.Instances.Real.Lemmas` `Mathlib.Topology.Instances.RealVectorSpace` `Mathlib.Topology.Instances.TrivSqZeroExt` `Mathlib.Topology.Instances.ZMultiples` `Mathlib.Topology.MetricSpace.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.Completion` `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.ContinuousMaps` `Mathlib.Topology.MetricSpace.Ultra.Pi` `Mathlib.Topology.MetricSpace.Ultra.TotallySeparated` `Mathlib.Topology.MetricSpace.UniformConvergence` `Mathlib.Topology.Metrizable.Basic` `Mathlib.Topology.Metrizable.CompletelyMetrizable` `Mathlib.Topology.Metrizable.ContinuousMap` `Mathlib.Topology.Metrizable.Real` `Mathlib.Topology.Metrizable.Uniformity` `Mathlib.Topology.Order.Real` `Mathlib.Topology.Path` `Mathlib.Topology.Semicontinuous` `Mathlib.Topology.Sheaves.CommRingCat` `Mathlib.Topology.UniformSpace.CompareReals` `Mathlib.Topology.UniformSpace.Dini` `Mathlib.Topology.UniformSpace.DiscreteUniformity` `Mathlib.Topology.UniformSpace.Matrix` `Mathlib.Topology.UniformSpace.ProdApproximation` `Mathlib.Topology.UniformSpace.Real` `Mathlib.Topology.UnitInterval`	-1

Declarations diff

+ cast_mul_floor_div_cancel
+ cast_mul_floor_div_cancel_of_pos
+ floor_div_cast_of_nonneg
+ floor_div_natCast
+ mul_cast_floor_div_cancel
+ mul_cast_floor_div_cancel_of_pos
+ mul_natCast_floor_div_cancel
+ natCast_mul_floor_div_cancel

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

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

The 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).

Ruben-VandeVelde

Thanks!

Mathlib/Algebra/Order/Floor/Semiring.lean

Mathlib/Data/Nat/Cast/Order/Field.lean

Mathlib/Algebra/Order/Floor/Semiring.lean

Mathlib/Data/Nat/Cast/Order/Field.lean

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Mathlib/Algebra/Order/Floor/Semiring.lean

YaelDillies · 2025-06-24T20:41:39Z

The import increase looks pretty bad. Do you have an idea how to avoid it?

vasnesterov · 2025-06-24T21:20:09Z

I think the Data/Int/Cast directory should mirror Data/Nat/Cast, and cast_div_le should be in Data.Int.Cast.Order.Field.

YaelDillies · 2025-06-24T21:23:45Z

I think the Data.Int.Cast and Data.Nat.Cast should not exist 😅: they are about algebra, not data

vasnesterov · 2025-06-26T10:58:53Z

@YaelDillies what should I do? I feel like refactoring the directory structure is too much for me :)
Should I create Data.Int.Cast.Order.Field for cast_div_le?

YaelDillies · 2025-06-26T12:23:17Z

I could golf proofs a bit further 😀

@YaelDillies what should I do? I feel like refactoring the directory structure is too much for me :) Should I create Data.Int.Cast.Order.Field for cast_div_le?

Would you mind moving cast_div_le/cast_div_ge to another PR? They are now both unnecessary for your titular result, and further review is necessary (cast_div_ge is still misnamed, and the import increase is really quite huge)

vasnesterov · 2025-06-26T13:19:26Z

OK, no problem

YaelDillies · 2025-06-26T13:24:39Z

Great, thanks!

maintainer merge

github-actions · 2025-06-26T13:24:53Z

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

Mathlib/Algebra/Order/Floor/Ring.lean

jcommelin · 2025-07-02T03:08:20Z

Thanks 🎉

bors merge

Prove that `⌊n * x⌋₊ / n = ⌊x⌋₊` for natural `n`. Co-authored-by: Vasilii Nesterov <118051017+vasnesterov@users.noreply.github.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

mathlib-bors · 2025-07-02T03:33:28Z

Pull request successfully merged into master.

Build succeeded:

CI Success

…y#26004) Prove that `⌊n * x⌋₊ / n = ⌊x⌋₊` for natural `n`. Co-authored-by: Vasilii Nesterov <118051017+vasnesterov@users.noreply.github.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

init

5bc4677

vasnesterov changed the title ~~feat(Algebra/Order/Floor): ⌊b * y⌋₊ / b = ⌊y⌋₊~~ feat(Algebra/Order/Floor): ⌊n * x⌋₊ / n = ⌊x⌋₊ Jun 17, 2025

vasnesterov added the t-algebra Algebra (groups, rings, fields, etc) label Jun 17, 2025

vasnesterov mentioned this pull request Jun 17, 2025

[Merged by Bors] - feat(Data/Real): representation of reals from [0, 1] in positional system #26021

Closed

1 task

Ruben-VandeVelde requested changes Jun 20, 2025

View reviewed changes

Mathlib/Algebra/Order/Floor/Semiring.lean Outdated Show resolved Hide resolved

Mathlib/Data/Nat/Cast/Order/Field.lean Outdated Show resolved Hide resolved

Ruben-VandeVelde added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 20, 2025

suggestions

d1f5802

vasnesterov removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 20, 2025

vasnesterov requested a review from Ruben-VandeVelde June 21, 2025 17:01

eric-wieser reviewed Jun 22, 2025

View reviewed changes

Mathlib/Algebra/Order/Floor/Semiring.lean Outdated Show resolved Hide resolved

eric-wieser requested a review from YaelDillies June 22, 2025 23:19

eric-wieser added the t-order Order theory label Jun 22, 2025

YaelDillies reviewed Jun 23, 2025

View reviewed changes

Mathlib/Data/Nat/Cast/Order/Field.lean Outdated Show resolved Hide resolved

vasnesterov and others added 2 commits June 23, 2025 15:10

tightness

7019e91

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Int version

e2c0635

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

more Int versions

b51c5eb

YaelDillies reviewed Jun 24, 2025

View reviewed changes

Mathlib/Algebra/Order/Floor/Semiring.lean Outdated Show resolved Hide resolved

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 24, 2025

right versions

e02e099

vasnesterov removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 24, 2025

Merge branch 'master' into Nat.cast_div

a880790

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 26, 2025

golf

019eabd

golf further

bff58f1

remove cast_div_le and cast_div_ge

e3e5786

vasnesterov removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 26, 2025

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

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 26, 2025

vasnesterov added 2 commits June 26, 2025 16:55

shake

214a94b

import Mathlib.Data.Nat.Cast.Order.Field

773a909

eric-wieser reviewed Jun 26, 2025

View reviewed changes

Mathlib/Algebra/Order/Floor/Ring.lean Outdated Show resolved Hide resolved

vasnesterov and others added 2 commits June 26, 2025 23:11

Merge branch 'master' into Nat.cast_div

e573370

mul_natCast_floor_div_cancel

322b333

b-mehta reviewed Jun 27, 2025

View reviewed changes

Mathlib/Algebra/Order/Floor/Ring.lean Outdated Show resolved Hide resolved

move

423f28a

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jul 2, 2025

mathlib-bors bot changed the title ~~feat(Algebra/Order/Floor): ⌊n * x⌋₊ / n = ⌊x⌋₊~~ [Merged by Bors] - feat(Algebra/Order/Floor): ⌊n * x⌋₊ / n = ⌊x⌋₊ Jul 2, 2025

mathlib-bors bot closed this Jul 2, 2025

Conversation

vasnesterov commented Jun 17, 2025 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 7260822b74

Import changes for modified files

Declarations diff

Uh oh!

Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies commented Jun 24, 2025

Uh oh!

vasnesterov commented Jun 24, 2025

Uh oh!

YaelDillies commented Jun 24, 2025

Uh oh!

vasnesterov commented Jun 26, 2025

Uh oh!

YaelDillies commented Jun 26, 2025

Uh oh!

vasnesterov commented Jun 26, 2025

Uh oh!

YaelDillies commented Jun 26, 2025

Uh oh!

github-actions bot commented Jun 26, 2025

Uh oh!

Uh oh!

Uh oh!

jcommelin commented Jul 2, 2025

Uh oh!

mathlib-bors bot commented Jul 2, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

vasnesterov commented Jun 17, 2025 •

edited by YaelDillies

Loading

github-actions bot commented Jun 17, 2025 •

edited

Loading