Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-08-07 10:57
30dd0d40
View on Github →
chore: backports for leanprover/lean4
#4814
(part 25) (
#15537
)
Estimated changes
Modified
Mathlib/Algebra/Lie/Submodule.lean
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
Modified
Mathlib/Analysis/InnerProductSpace/Orientation.lean
Modified
Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean
Modified
Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean
Modified
Mathlib/Analysis/Normed/Lp/PiLp.lean
modified
def
LinearIsometryEquiv.piLpCurry
Modified
Mathlib/Analysis/NormedSpace/DualNumber.lean
Modified
Mathlib/Combinatorics/Additive/Corner/Roth.lean
Modified
Mathlib/FieldTheory/Perfect.lean
Modified
Mathlib/Geometry/Manifold/InteriorBoundary.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean
Modified
Mathlib/LinearAlgebra/Trace.lean
Modified
Mathlib/MeasureTheory/Constructions/Pi.lean
modified
theorem
MeasureTheory.measurePreserving_pi
modified
theorem
MeasureTheory.measurePreserving_piFinsetUnion
modified
theorem
MeasureTheory.volume_preserving_piFinsetUnion
Modified
Mathlib/MeasureTheory/Constructions/Prod/Basic.lean
modified
theorem
MeasureTheory.Measure.ae_ae_eq_curry_of_prod
modified
theorem
MeasureTheory.Measure.ae_ae_eq_of_ae_eq_uncurry
Modified
Mathlib/MeasureTheory/Group/Measure.lean
Modified
Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean
modified
theorem
MeasureTheory.measure_of_cont_bdd_of_tendsto_indicator
Modified
Mathlib/RingTheory/Kaehler/Basic.lean
modified
theorem
KaehlerDifferential.kerTotal_map'
modified
theorem
KaehlerDifferential.kerTotal_map
Modified
Mathlib/RingTheory/Unramified/Finite.lean
modified
theorem
Algebra.FormallyUnramified.lmul_elem
Modified
Mathlib/RingTheory/WittVector/Basic.lean
Modified
Mathlib/RingTheory/WittVector/InitTail.lean
Modified
Mathlib/RingTheory/WittVector/Teichmuller.lean
Modified
Mathlib/RingTheory/WittVector/Verschiebung.lean
modified
theorem
WittVector.ghostComponent_verschiebungFun
modified
theorem
WittVector.ghostComponent_zero_verschiebungFun
modified
theorem
WittVector.verschiebung_isPoly
Modified
Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
modified
theorem
GromovHausdorff.candidatesBDist_mem_candidatesB