Commit 2024-08-08 10:31 2edef7d5

View on Github →

chore: backports for leanprover/lean4#4814 (part 36) (#15612)

Estimated changes

Modified Archive/Imo/Imo1975Q1.lean

modified theorem imo1975_q1

Modified Archive/Imo/Imo2019Q2.lean

modified theorem Imo2019Q2.Imo2019q2Cfg.oangle_CQ₁Q_eq_oangle_CBA

modified theorem Imo2019Q2.Imo2019q2Cfg.oangle_CQ₁Q_sign_eq_oangle_CBA_sign

modified def Imo2019Q2.someOrientation

modified theorem imo2019_q2

Modified Archive/Imo/Imo2024Q2.lean

Modified Archive/Wiedijk100Theorems/BuffonsNeedle.lean

Modified Archive/Wiedijk100Theorems/CubingACube.lean

Modified Archive/Wiedijk100Theorems/SolutionOfCubic.lean

Modified Archive/ZagierTwoSquares.lean

Modified Counterexamples/QuadraticForm.lean

modified theorem Counterexample.B_ne_zero

modified theorem Counterexample.isAlt_B

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

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

Modified Mathlib/Analysis/CStarAlgebra/Module.lean

Modified Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

modified theorem Real.pow_mul_norm_iteratedFDeriv_fourierIntegral_le

Modified Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean

modified theorem MeasureTheory.GridLines.T_insert_le_T_lmarginal_singleton

modified theorem MeasureTheory.GridLines.T_lmarginal_antitone

modified theorem MeasureTheory.GridLines.T_univ

modified theorem MeasureTheory.lintegral_mul_prod_lintegral_pow_le

modified theorem MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux

modified theorem MeasureTheory.lintegral_prod_lintegral_pow_le

Modified Mathlib/Geometry/Manifold/BumpFunction.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/Basic.lean

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

Modified Mathlib/NumberTheory/Cyclotomic/Rat.lean

Modified Mathlib/NumberTheory/Cyclotomic/Three.lean

modified theorem IsCyclotomicExtension.Rat.Three.Units.mem

modified theorem IsCyclotomicExtension.Rat.Three.eq_one_or_neg_one_of_unit_of_congruent

modified theorem IsCyclotomicExtension.Rat.Three.lambda_dvd_or_dvd_sub_one_or_dvd_add_one

Modified Mathlib/NumberTheory/FLT/Three.lean

modified theorem FermatLastTheoremForThree_of_FermatLastTheoremThreeGen

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

modified theorem NumberField.InfinitePlace.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq

modified theorem NumberField.InfinitePlace.exists_smul_eq_of_comap_eq

Modified Mathlib/NumberTheory/NumberField/EquivReindex.lean

modified theorem NumberField.det_of_basisMatrix_non_zero

modified theorem NumberField.inverse_basisMatrix_mulVec_eq_repr

Modified Mathlib/NumberTheory/NumberField/House.lean

Modified Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean