Commit 2024-08-02 06:24 b941d5ea

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/BigOperators/Finsupp.lean

modified theorem Finsupp.sum_sum_index'

Modified Mathlib/Algebra/Homology/Embedding/Restriction.lean

Modified Mathlib/Algebra/Lie/Basic.lean

Modified Mathlib/Algebra/Module/Submodule/Range.lean

modified theorem Submodule.coe_mapIic_apply

modified def Submodule.mapIic

Modified Mathlib/CategoryTheory/Limits/FinallySmall.lean

modified theorem CategoryTheory.finallySmall_of_final_of_essentiallySmall

modified theorem CategoryTheory.finallySmall_of_final_of_finallySmall

modified theorem CategoryTheory.initiallySmall_of_initial_of_essentiallySmall

modified theorem CategoryTheory.initiallySmall_of_initial_of_initiallySmall

Modified Mathlib/CategoryTheory/Limits/Presheaf.lean

Modified Mathlib/CategoryTheory/Localization/DerivabilityStructure/Constructor.lean

modified theorem CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.mk'

Modified Mathlib/CategoryTheory/Shift/InducedShiftSequence.lean

Modified Mathlib/CategoryTheory/Sites/Adjunction.lean

modified def CategoryTheory.Sheaf.adjunction

modified def CategoryTheory.Sheaf.composeEquiv

Modified Mathlib/CategoryTheory/Sites/CoverLifting.lean

modified def CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility

Modified Mathlib/Data/Finite/Card.lean

modified theorem Set.Finite.eq_of_subset_of_card_le

Modified Mathlib/Data/Finset/Pointwise.lean

modified def Finset.imageMulHom

modified theorem Finset.image_mul

modified theorem Finset.inf_mul_left

modified theorem Finset.inf_mul_right

modified theorem Finset.isUnit_iff_singleton_aux

modified theorem Finset.le_inf_mul

modified theorem Finset.sup_mul_le

modified theorem Finset.sup_mul_left

modified theorem Finset.sup_mul_right

Modified Mathlib/Data/Int/CardIntervalMod.lean

Modified Mathlib/Data/Matroid/Basic.lean

modified theorem Matroid.ExchangeProperty.antichain

modified theorem Matroid.ExchangeProperty.encard_base_eq

modified theorem Matroid.ExchangeProperty.encard_diff_eq

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

modified theorem MultilinearMap.domDomRestrict_aux

modified theorem MultilinearMap.domDomRestrict_aux_right

modified theorem MultilinearMap.iteratedFDeriv_aux

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

modified theorem measurable_uniqueElim

Modified Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean

Modified Mathlib/Topology/Constructions.lean

modified theorem Filter.Tendsto.fst_nhds

modified theorem Filter.Tendsto.snd_nhds

modified theorem prod_induced_induced

Modified Mathlib/Topology/ContinuousOn.lean

modified theorem continuousOn_to_generateFrom_iff