Commit 2024-08-09 00:58 0f7bb9cc

View on Github →

chore: backports for leanprover/lean4#4814 (part 33) (#15605)

Estimated changes

Modified Mathlib/Algebra/Homology/DerivedCategory/Ext.lean

Modified Mathlib/Algebra/Lie/CartanExists.lean

modified theorem LieAlgebra.engel_isBot_of_isMin.lieCharpoly_coeff_natDegree

modified theorem LieAlgebra.engel_isBot_of_isMin.lieCharpoly_natDegree

Modified Mathlib/Algebra/Lie/Killing.lean

modified theorem LieAlgebra.IsKilling.ideal_eq_bot_of_isLieAbelian

Modified Mathlib/Algebra/Lie/Weights/Linear.lean

modified theorem LieModule.exists_forall_lie_eq_smul

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unitary.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

Modified Mathlib/Analysis/Fourier/AddCircle.lean

Modified Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean

modified theorem RCLike.re_extendTo𝕜'ₗ

Modified Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

modified theorem SimpleGraph.degree_eq_sum_if_adj

Modified Mathlib/Geometry/Manifold/ContMDiff/NormedSpace.lean

Modified Mathlib/Geometry/Manifold/ContMDiff/Product.lean

Modified Mathlib/LinearAlgebra/Matrix/SchurComplement.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean

modified theorem exists_spanning_measurableSet_le

Modified Mathlib/MeasureTheory/Constructions/Polish/Basic.lean

Modified Mathlib/MeasureTheory/Function/ContinuousMapDense.lean

modified theorem BoundedContinuousFunction.toLp_denseRange

modified theorem ContinuousMap.toLp_denseRange

modified theorem MeasureTheory.Memℒp.exists_hasCompactSupport_eLpNorm_sub_le

Modified Mathlib/MeasureTheory/Group/Integral.lean

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

Modified Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean

modified theorem BoundedContinuousFunction.integrable_of_nnreal

modified theorem BoundedContinuousFunction.integral_eq_integral_nnrealPart_sub

modified theorem BoundedContinuousFunction.measurable_coe_ennreal_comp

modified theorem BoundedContinuousFunction.toReal_lintegral_coe_eq_integral

Modified Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean

modified theorem LinearIsometryEquiv.measurePreserving

Modified Mathlib/NumberTheory/Cyclotomic/Basic.lean

modified theorem CyclotomicRing.algebraBase_injective

Modified Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

modified theorem IsIntegralClosure.isLocalization

modified theorem IsIntegralClosure.isLocalization_of_isSeparable

Modified Mathlib/RingTheory/Discriminant.lean

modified theorem Algebra.discr_eq_discr

Modified Mathlib/RingTheory/Kaehler/Basic.lean

Modified Mathlib/RingTheory/WittVector/MulCoeff.lean

modified theorem WittVector.mul_polyOfInterest_aux3

Modified Mathlib/Topology/Algebra/Algebra.lean