Commit 2024-08-21 08:17 22e3994a

View on Github →

chore: more byAsSorry backports (#15972)

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

modified def ModuleCat.restrictScalarsComp'App

modified def ModuleCat.restrictScalarsId'App

Modified Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean

modified def PresheafOfModules.Derivation'.mk

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean

modified def PresheafOfModules.sheafifyMap

Modified Mathlib/Algebra/Category/ModuleCat/Sheaf/ChangeOfRings.lean

Modified Mathlib/Algebra/Lie/InvariantForm.lean

modified def LieAlgebra.InvariantForm.orthogonal

Modified Mathlib/Algebra/Module/Zlattice/Basic.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

modified def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier

Modified Mathlib/Analysis/ConstantSpeed.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean

Modified Mathlib/Analysis/InnerProductSpace/l2Space.lean

Modified Mathlib/CategoryTheory/Preadditive/Schur.lean

Modified Mathlib/Data/Complex/FiniteDimensional.lean

Modified Mathlib/Data/Fin/Basic.lean

Modified Mathlib/Data/Int/Interval.lean

Modified Mathlib/Data/List/DropRight.lean

Modified Mathlib/Data/List/Nodup.lean

Modified Mathlib/Data/List/Range.lean

Modified Mathlib/Data/Matrix/Kronecker.lean

Modified Mathlib/Data/NNReal/Basic.lean

Modified Mathlib/Data/Set/Function.lean

Modified Mathlib/FieldTheory/KummerExtension.lean

modified def adjoinRootXPowSubCEquiv

Modified Mathlib/FieldTheory/PerfectClosure.lean

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

Modified Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

modified def AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSheafedSpace

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/Lagrange.lean

modified theorem Lagrange.X_sub_C_dvd_nodal

Modified Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

Modified Mathlib/MeasureTheory/Function/L1Space.lean

Modified Mathlib/MeasureTheory/Function/L2Space.lean

Modified Mathlib/MeasureTheory/Group/Prod.lean

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

Modified Mathlib/NumberTheory/Cyclotomic/Gal.lean

Modified Mathlib/NumberTheory/Cyclotomic/Rat.lean

modified theorem IsPrimitiveRoot.subOneIntegralPowerBasis'_gen

Modified Mathlib/Probability/ProbabilityMassFunction/Integrals.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean

Modified Mathlib/RingTheory/AdicCompletion/Exactness.lean

modified theorem AdicCompletion.map_surjective

Modified Mathlib/RingTheory/Adjoin/Field.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

modified def IsAdjoinRoot.lift

Modified Mathlib/RingTheory/SimpleModule.lean

Modified Mathlib/RingTheory/WittVector/Compare.lean

Modified Mathlib/SetTheory/Game/Short.lean