Commit 2024-08-09 00:58 f248f7db

View on Github →

chore: backports for leanprover/lean4#4814 (part 24) (#15520)

Estimated changes

Modified Mathlib/Algebra/Module/LinearMap/Polynomial.lean

modified theorem LinearMap.isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank

modified theorem LinearMap.nilRank_le_card

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean

modified theorem WeierstrassCurve.Affine.addX_eq_addX_negY_sub

modified theorem WeierstrassCurve.Affine.addY_sub_negY_addY

modified theorem WeierstrassCurve.Affine.cyclic_sum_Y_mul_X_sub_X

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

Modified Mathlib/Analysis/Convex/Body.lean

Modified Mathlib/Analysis/Convex/GaugeRescale.lean

Modified Mathlib/Analysis/InnerProductSpace/Rayleigh.lean

modified theorem LinearMap.IsSymmetric.hasEigenvalue_iInf_of_finiteDimensional

modified theorem LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional

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

Modified Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean

Modified Mathlib/GroupTheory/PushoutI.lean

modified theorem Monoid.PushoutI.NormalWord.prod_injective

modified theorem Monoid.PushoutI.Reduced.eq_empty_of_mem_range

modified theorem Monoid.PushoutI.inf_of_range_eq_base_range

Modified Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

modified theorem LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict

Modified Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean

Modified Mathlib/LinearAlgebra/Charpoly/Basic.lean

modified theorem LinearMap.charpoly_natDegree

modified theorem LinearMap.minpoly_coeff_zero_of_injective

Modified Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean

Modified Mathlib/LinearAlgebra/Contraction.lean

Modified Mathlib/LinearAlgebra/Orientation.lean

modified theorem Orientation.eq_or_eq_neg

modified theorem Orientation.map_eq_det_inv_smul

modified theorem Orientation.map_eq_iff_det_pos

modified theorem Orientation.ne_iff_eq_neg

modified def Orientation.someBasis

modified theorem Orientation.someBasis_orientation

Modified Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean

Modified Mathlib/MeasureTheory/Function/AEEqFun.lean

modified theorem MeasureTheory.AEEqFun.compMeasurePreserving_toGerm

modified theorem MeasureTheory.AEEqFun.compQuasiMeasurePreserving_toGerm

modified theorem MeasureTheory.AEEqFun.comp_compQuasiMeasurePreserving

Modified Mathlib/MeasureTheory/Function/SpecialFunctions/Arctan.lean

modified theorem Measurable.arctan

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

modified theorem MeasureTheory.tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure

Modified Mathlib/MeasureTheory/Measure/AEMeasurable.lean

modified theorem aemeasurable_of_map_neZero

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

modified theorem MeasurableSpace.ae_induction_on_inter

Modified Mathlib/MeasureTheory/Measure/OpenPos.lean

Modified Mathlib/MeasureTheory/Order/Group/Lattice.lean

modified theorem measurable_leOnePart

modified theorem measurable_oneLePart

Modified Mathlib/NumberTheory/Rayleigh.lean

Modified Mathlib/NumberTheory/SiegelsLemma.lean

modified theorem Int.Matrix.exists_ne_zero_int_vec_norm_le'

modified theorem Int.Matrix.exists_ne_zero_int_vec_norm_le

Modified Mathlib/RingTheory/AdicCompletion/Functoriality.lean

modified def AdicCompletion.sum

modified theorem AdicCompletion.sum_lof

modified theorem AdicCompletion.sum_of

Modified Mathlib/RingTheory/Adjoin/Field.lean

modified theorem IsIntegral.mem_range_algHom_of_minpoly_splits

modified theorem IsIntegral.mem_range_algebraMap_of_minpoly_splits

modified theorem IsIntegral.minpoly_splits_tower_top'

modified theorem IsIntegral.minpoly_splits_tower_top

Modified Mathlib/RingTheory/Algebraic.lean

modified theorem Algebra.IsAlgebraic.algHom_bijective

modified theorem Algebra.IsAlgebraic.algHom_bijective₂

modified theorem Algebra.IsAlgebraic.bijective_of_isScalarTower

Modified Mathlib/RingTheory/Artinian.lean

Modified Mathlib/RingTheory/EssentialFiniteness.lean

Modified Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean

modified theorem IsIntegral.smul

Modified Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean

modified theorem IsIntegrallyClosed.algebraMap_eq_of_integral

modified theorem IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow

modified theorem IsIntegrallyClosed.integralClosure_eq_bot

modified theorem IsIntegrallyClosed.isIntegral_iff

modified theorem IsIntegrallyClosed.pow_dvd_pow_iff

modified theorem IsIntegrallyClosedIn.algebraMap_eq_of_integral

modified theorem IsIntegrallyClosedIn.exists_algebraMap_eq_of_isIntegral_pow

modified theorem IsIntegrallyClosedIn.integralClosure_eq_bot

modified theorem IsIntegrallyClosedIn.isIntegral_iff

Modified Mathlib/RingTheory/Kaehler/CotangentComplex.lean

Modified Mathlib/RingTheory/Localization/BaseChange.lean

Modified Mathlib/RingTheory/PowerBasis.lean

Modified Mathlib/RingTheory/Regular/RegularSequence.lean

modified theorem LinearEquiv.isRegular_congr

modified theorem LinearEquiv.isWeaklyRegular_congr

Modified Mathlib/RingTheory/SurjectiveOnStalks.lean

modified theorem RingHom.surjectiveOnStalks_of_isLocalization

Modified Mathlib/RingTheory/TensorProduct/MvPolynomial.lean

Modified Mathlib/RingTheory/Trace/Defs.lean

modified theorem Algebra.traceForm_toMatrix

modified theorem Algebra.trace_algebraMap_of_basis

Modified Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean

modified theorem compactlyGeneratedSpace_of_coinduced

modified theorem continuous_from_compactlyGenerated

Modified Mathlib/Topology/ContinuousFunction/Ideals.lean

Modified Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean

Modified Mathlib/Topology/VectorBundle/Hom.lean

modified theorem Pretrivialization.continuousOn_continuousLinearMapCoordChange