Commit 2024-08-01 16:02 786a0509

View on Github →

chore: backports for leanprover/lean4#4814 (part 9) (#15389) see https://github.com/leanprover-community/mathlib4/pull/15245

Estimated changes

Modified Mathlib/Algebra/BigOperators/Ring.lean

modified theorem Commute.sum_left

modified theorem Commute.sum_right

modified theorem Finset.prod_add_ordered

modified theorem Finset.sum_pow'

modified theorem Fintype.prod_sum

Modified Mathlib/Algebra/BigOperators/WithTop.lean

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

modified theorem GenContFract.IntFractPair.coe_of_rat_eq

modified theorem GenContFract.IntFractPair.coe_stream'_rat_eq

modified theorem GenContFract.IntFractPair.coe_stream_nth_rat_eq

modified theorem GenContFract.coe_of_h_rat_eq

modified theorem GenContFract.coe_of_rat_eq

modified theorem GenContFract.coe_of_s_get?_rat_eq

modified theorem GenContFract.coe_of_s_rat_eq

Modified Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

Modified Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean

Modified Mathlib/Analysis/Normed/Group/Seminorm.lean

Modified Mathlib/CategoryTheory/Abelian/Transfer.lean

modified def CategoryTheory.AbelianOfAdjunction.coimageIsoImage

modified def CategoryTheory.AbelianOfAdjunction.coimageIsoImageAux

modified theorem CategoryTheory.AbelianOfAdjunction.coimageIsoImage_hom

modified def CategoryTheory.AbelianOfAdjunction.cokernelIso

modified theorem CategoryTheory.AbelianOfAdjunction.hasCokernels

modified theorem CategoryTheory.AbelianOfAdjunction.hasKernels

Modified Mathlib/CategoryTheory/GlueData.lean

Modified Mathlib/CategoryTheory/Localization/StructuredArrow.lean

modified theorem CategoryTheory.Localization.induction_costructuredArrow

modified theorem CategoryTheory.Localization.induction_structuredArrow

Modified Mathlib/CategoryTheory/Shift/Localization.lean

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

modified theorem SimpleGraph.deleteFar_iff

Modified Mathlib/Combinatorics/SimpleGraph/Operations.lean

Modified Mathlib/Computability/RegularExpressions.lean

Modified Mathlib/Data/Finset/NAry.lean

modified theorem Finset.image₂_assoc

Modified Mathlib/Data/Finset/Sym.lean

modified theorem Finset.image_diag_union_image_offDiag

Modified Mathlib/Data/Fintype/Pi.lean

modified theorem Finset.Nonempty.piFinset_const

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

modified theorem MulAction.le_stabilizer_smul_right

Modified Mathlib/GroupTheory/Perm/ClosureSwap.lean

Modified Mathlib/Order/Birkhoff.lean

modified theorem OrderEmbedding.birkhoffSet_apply

Modified Mathlib/Order/Interval/Finset/Basic.lean

Modified Mathlib/Order/Interval/Finset/Box.lean

Modified Mathlib/Order/Interval/Finset/Defs.lean

modified theorem Finset.map_subtype_embedding_Ici

modified theorem Finset.map_subtype_embedding_Iic

modified theorem Finset.map_subtype_embedding_Iio

modified theorem Finset.map_subtype_embedding_Ioi

Modified Mathlib/Order/Interval/Finset/Nat.lean

modified theorem Nat.cauchy_induction

modified theorem Nat.cauchy_induction_two_mul

modified theorem Nat.decreasing_induction_of_infinite

modified theorem Nat.decreasing_induction_of_not_bddAbove

Modified Mathlib/Order/LiminfLimsup.lean

Modified Mathlib/Topology/Basic.lean

modified theorem TopologicalSpace.ext_iff_isClosed

modified theorem TopologicalSpace.ext_iff_nhds

Modified Mathlib/Topology/Order.lean

modified theorem continuous_discrete_rng