Commit 2024-01-15 00:29 1d3b4790

View on Github →

fix: shake the import tree (#9749) cherry-picked from #9347 Co-Authored-By: @digama0

Estimated changes

Modified Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/Order/Field/Pi.lean

Modified Mathlib/Algebra/Order/Floor.lean

Modified Mathlib/Algebra/Order/Sub/Prod.lean

Modified Mathlib/Analysis/BoxIntegral/Basic.lean

Modified Mathlib/Analysis/SpecificLimits/IsROrC.lean

Modified Mathlib/CategoryTheory/Abelian/Projective.lean

Modified Mathlib/CategoryTheory/Preadditive/Yoneda/Projective.lean

Modified Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean

Modified Mathlib/Computability/Ackermann.lean

Modified Mathlib/Control/Monad/Basic.lean

Modified Mathlib/Data/Array/Basic.lean

Modified Mathlib/Data/Finset/Pointwise/Interval.lean

Modified Mathlib/Data/Fintype/Small.lean

Modified Mathlib/Data/Nat/Choose/Bounds.lean

Modified Mathlib/Data/Nat/Factorization/Basic.lean

Modified Mathlib/Data/Num/Basic.lean

Modified Mathlib/Data/Polynomial/Degree/CardPowDegree.lean

Modified Mathlib/Data/Real/ENNReal.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Data/UnionFind.lean

Modified Mathlib/Init/Control/Lawful.lean

modified theorem OptionT.ext

Modified Mathlib/Init/Data/Int/Basic.lean

Modified Mathlib/Init/Data/Int/Bitwise.lean

Modified Mathlib/Init/Data/Int/CompLemmas.lean

Modified Mathlib/Init/Data/Nat/GCD.lean

Modified Mathlib/Init/IteSimp.lean

Modified Mathlib/Init/Meta/WellFoundedTactics.lean

Modified Mathlib/Lean/Elab/Term.lean

Modified Mathlib/NumberTheory/LucasLehmer.lean

Modified Mathlib/NumberTheory/Multiplicity.lean

Modified Mathlib/NumberTheory/PellMatiyasevic.lean

Modified Mathlib/NumberTheory/PythagoreanTriples.lean

Modified Mathlib/Probability/Distributions/Gaussian.lean

Modified Mathlib/Probability/Distributions/Poisson.lean

Modified Mathlib/Probability/Notation.lean

Modified Mathlib/RingTheory/QuotientNoetherian.lean

Modified Mathlib/RingTheory/Valuation/Basic.lean

Modified Mathlib/Tactic/Attr/Register.lean

Modified Mathlib/Tactic/Continuity.lean

Modified Mathlib/Tactic/Existsi.lean

Modified Mathlib/Tactic/HigherOrder.lean

Modified Mathlib/Tactic/Linarith/Lemmas.lean

Modified Mathlib/Tactic/ReduceModChar/Ext.lean

Modified Mathlib/Topology/Algebra/Semigroup.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean

Modified Mathlib/Topology/LocalExtr.lean

Modified Mathlib/Topology/Support.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean