Commit 2024-08-07 07:08 45121e17

View on Github →

chore: backports for leanprover/lean4#4814 (part 23) (#15514)

Estimated changes

Modified Mathlib/Algebra/DirectSum/LinearMap.lean

modified theorem LinearMap.mapsTo_biSup_of_mapsTo

modified theorem LinearMap.trace_eq_sum_trace_restrict'

modified theorem LinearMap.trace_eq_sum_trace_restrict

modified theorem LinearMap.trace_eq_zero_of_mapsTo_ne

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

modified theorem ApproximatesLinearOn.surjOn_closedBall_of_nonlinearRightInverse

Modified Mathlib/Analysis/Calculus/LHopital.lean

modified theorem HasDerivAt.lhopital_zero_left_on_Ioc

modified theorem HasDerivAt.lhopital_zero_left_on_Ioo

modified theorem HasDerivAt.lhopital_zero_right_on_Ico

modified theorem HasDerivAt.lhopital_zero_right_on_Ioo

modified theorem deriv.lhopital_zero_left_on_Ioo

modified theorem deriv.lhopital_zero_right_on_Ico

modified theorem deriv.lhopital_zero_right_on_Ioo

Modified Mathlib/Analysis/Matrix.lean

Modified Mathlib/Condensed/Epi.lean

Modified Mathlib/FieldTheory/Cardinality.lean

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

modified theorem Manifold.locallyCompact_of_finiteDimensional

Modified Mathlib/LinearAlgebra/BilinearForm/Properties.lean

modified theorem LinearMap.BilinForm.IsRefl.eq_zero

modified theorem LinearMap.BilinForm.IsSymm.isRefl

modified theorem LinearMap.BilinForm.dualBasis_dualBasis_flip

modified theorem LinearMap.BilinForm.dualBasis_repr_apply

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

modified theorem Algebra.IsIntegral.of_injective

Modified Mathlib/RingTheory/LocalRing/Module.lean

modified theorem LocalRing.split_injective_iff_lTensor_residueField_injective

modified theorem Module.free_of_lTensor_residueField_injective

Modified Mathlib/RingTheory/Localization/Cardinality.lean

modified theorem IsLocalization.card

modified theorem IsLocalization.card_le