Commit 2025-12-31 20:48 b6248267

View on Github →

chore(Algebra/Order/Floor): review API about round (#33421)

Estimated changes

Modified Mathlib/Algebra/AddConstMap/Basic.lean

Modified Mathlib/Algebra/Order/Archimedean/Basic.lean

Modified Mathlib/Algebra/Order/Floor/Ring.lean

added theorem Int.ceil_intCast_add

added theorem Int.ceil_natCast_add

added theorem Int.ceil_ofNat_add

added theorem Int.ceil_one_add

added theorem Int.mul_fract_eq_one_iff_exists_int

Modified Mathlib/Algebra/Order/Round.lean

added theorem round_eq_div

added theorem round_eq_half_ceil_two_mul

added theorem round_eq_iff

modified theorem round_neg_two_inv

modified theorem round_two_inv

Modified Mathlib/Algebra/Order/ToIntervalMod.lean

Modified Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean

Modified Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean

Modified Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean

Modified Mathlib/GroupTheory/Archimedean.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/DerivIntegrable.lean

Modified Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean

Modified Mathlib/Order/Filter/AtTopBot/Archimedean.lean

Modified Mathlib/Topology/Algebra/Order/Floor.lean

Modified Mathlib/Topology/Instances/AddCircle/Defs.lean