Commit 2024-05-01 22:18 4c031bc4

View on Github →

chore: adaptations to lean 4.8.0 (#12583) Mainly this adds names to instances, which are presumably necessary for some unspecified reason.

Estimated changes

Modified Mathlib/Analysis/Complex/Basic.lean

Modified Mathlib/Analysis/NormedSpace/AffineIsometry.lean

Modified Mathlib/Data/Complex/Module.lean

Modified Mathlib/Data/Finsupp/Notation.lean

Modified Mathlib/Data/Rat/Order.lean

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean

Modified Mathlib/NumberTheory/ZetaFunction.lean

Modified Mathlib/Order/Booleanisation.lean

Modified Mathlib/RingTheory/Ideal/Colon.lean

Modified Mathlib/RingTheory/Ideal/Quotient.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean

Modified Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

Modified Mathlib/RingTheory/PowerSeries/Order.lean

Modified Mathlib/RingTheory/Valuation/RankOne.lean

Modified Mathlib/Topology/Algebra/GroupCompletion.lean

Modified Mathlib/Topology/Algebra/Module/Basic.lean

Modified Mathlib/Topology/Algebra/Ring/Basic.lean

Modified Mathlib/Topology/Category/Stonean/Basic.lean

Modified Mathlib/Topology/ContinuousFunction/Bounded.lean

Modified Mathlib/Topology/Instances/Real.lean

Modified Mathlib/Topology/Order/ScottTopology.lean

Modified Mathlib/Topology/Sheaves/Skyscraper.lean

Modified Mathlib/Topology/UniformSpace/Matrix.lean

Modified docs/overview.yaml

Modified docs/undergrad.yaml

Modified test/Simps.lean

Modified test/ValuedCSP.lean

Modified test/byContra.lean

Modified test/instance_diamonds.lean

Modified test/instance_diamonds/normed.lean

Modified test/observe.lean

Modified test/propose.lean

Modified test/slim_check.lean