Commit 2024-08-01 00:14 83173e41

View on Github →

chore: backport some changes for lean v4.11.0 (#15368)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Cover/Open.lean

Modified Mathlib/AlgebraicGeometry/Properties.lean

Modified Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean

deleted theorem ContinuousLinearMapWOT.ext_dual_iff

Modified Mathlib/Analysis/NormedSpace/Pointwise.lean

Modified Mathlib/CategoryTheory/IsomorphismClasses.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Assoc.lean

Modified Mathlib/CategoryTheory/Thin.lean

Modified Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean

Modified Mathlib/Combinatorics/SimpleGraph/Trails.lean

Modified Mathlib/Computability/TuringMachine.lean

Modified Mathlib/Data/Fin/Basic.lean

modified theorem Fin.castSucc_zero'

Modified Mathlib/Data/LazyList/Basic.lean

Modified Mathlib/Data/List/Chain.lean

Modified Mathlib/Data/List/DropRight.lean

Modified Mathlib/Order/Chain.lean

Modified Mathlib/Probability/Kernel/Basic.lean

deleted theorem ProbabilityTheory.Kernel.ext_iff

Modified Mathlib/Probability/Kernel/RadonNikodym.lean

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

deleted theorem HahnModule.ext_iff

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

deleted theorem MvPowerSeries.ext_iff

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

deleted theorem PowerSeries.ext_iff

Modified Mathlib/RingTheory/PowerSeries/WellKnown.lean

Modified Mathlib/SetTheory/ZFC/Basic.lean

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

modified theorem Profinite.NobelingProof.GoodProducts.span_iff_products