Commit 2023-06-07 01:25 ea80818c

View on Github →

chore: tidy various files (#4757)

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean

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

Modified Mathlib/Analysis/MeanInequalities.lean

Modified Mathlib/Analysis/NormedSpace/AffineIsometry.lean

added theorem AffineIsometryEquiv.coe_constVAdd

added theorem AffineIsometryEquiv.coe_constVSub

deleted theorem AffineIsometryEquiv.coe_constVadd

deleted theorem AffineIsometryEquiv.coe_constVsub

added def AffineIsometryEquiv.constVAdd

added theorem AffineIsometryEquiv.constVAdd_zero

added def AffineIsometryEquiv.constVSub

deleted def AffineIsometryEquiv.constVadd

deleted theorem AffineIsometryEquiv.constVadd_zero

deleted def AffineIsometryEquiv.constVsub

added theorem AffineIsometryEquiv.symm_constVSub

deleted theorem AffineIsometryEquiv.symm_constVsub

Modified Mathlib/Analysis/NormedSpace/Dual.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean

Modified Mathlib/CategoryTheory/Abelian/LeftDerived.lean

deleted theorem CategoryTheory.Abelian.Functor.exact_of_map_ProjectiveResolution

added theorem CategoryTheory.Abelian.Functor.exact_of_map_projectiveResolution

Modified Mathlib/CategoryTheory/Abelian/RightDerived.lean

Modified Mathlib/CategoryTheory/Monoidal/Braided.lean

Modified Mathlib/FieldTheory/Finite/Basic.lean

deleted theorem ZMod.frobenius_zMod

added theorem ZMod.frobenius_zmod

Modified Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean

Modified Mathlib/LinearAlgebra/InvariantBasisNumber.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean

Modified Mathlib/MeasureTheory/Constructions/Prod/Integral.lean

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

Modified Mathlib/MeasureTheory/Group/Action.lean

Modified Mathlib/MeasureTheory/Integral/MeanInequalities.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean

Modified Mathlib/NumberTheory/Bernoulli.lean

Modified Mathlib/Probability/Independence/Basic.lean

Modified Mathlib/RingTheory/Artinian.lean

Modified Mathlib/RingTheory/Noetherian.lean

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

deleted theorem PontryaginDual.map_mul'

Modified Mathlib/Topology/Sheaves/Presheaf.lean