Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-08-17 17:28
916c75c1
View on Github →
chore: remove unused simps (
#6632
)
Estimated changes
Modified
Archive/Imo/Imo1988Q6.lean
Modified
Archive/Sensitivity.lean
Modified
Mathlib/Algebra/Associated.lean
Modified
Mathlib/Algebra/BigOperators/Basic.lean
Modified
Mathlib/Algebra/BigOperators/Ring.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
Modified
Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
Modified
Mathlib/Algebra/CharP/MixedCharZero.lean
Modified
Mathlib/Algebra/GeomSum.lean
Modified
Mathlib/Algebra/GroupPower/Basic.lean
Modified
Mathlib/Algebra/Homology/Homotopy.lean
Modified
Mathlib/Algebra/Module/Injective.lean
Modified
Mathlib/Algebra/Module/Torsion.lean
Modified
Mathlib/Algebra/Order/CompleteField.lean
Modified
Mathlib/Algebra/QuaternionBasis.lean
Modified
Mathlib/AlgebraicGeometry/AffineScheme.lean
Modified
Mathlib/AlgebraicGeometry/Gluing.lean
Modified
Mathlib/AlgebraicGeometry/LocallyRingedSpace.lean
Modified
Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean
Modified
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
Modified
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
Modified
Mathlib/AlgebraicTopology/CechNerve.lean
Modified
Mathlib/AlgebraicTopology/ExtraDegeneracy.lean
Modified
Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
Modified
Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean
Modified
Mathlib/AlgebraicTopology/SplitSimplicialObject.lean
Modified
Mathlib/Analysis/Analytic/Composition.lean
Modified
Mathlib/Analysis/Analytic/Inverse.lean
Modified
Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
Modified
Mathlib/Analysis/Calculus/LHopital.lean
Modified
Mathlib/Analysis/Convex/Between.lean
Modified
Mathlib/Analysis/Convex/Side.lean
Modified
Mathlib/Analysis/Distribution/SchwartzSpace.lean
Modified
Mathlib/Analysis/Fourier/PoissonSummation.lean
Modified
Mathlib/Analysis/InnerProductSpace/OfNorm.lean
Modified
Mathlib/Analysis/InnerProductSpace/Projection.lean
Modified
Mathlib/Analysis/Matrix.lean
modified
theorem
Matrix.nnnorm_transpose
Modified
Mathlib/Analysis/NormedSpace/Exponential.lean
Modified
Mathlib/Analysis/NormedSpace/OperatorNorm.lean
Modified
Mathlib/Analysis/NormedSpace/PiLp.lean
Modified
Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
Modified
Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gaussian.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
Modified
Mathlib/CategoryTheory/Abelian/LeftDerived.lean
Modified
Mathlib/CategoryTheory/CofilteredSystem.lean
Modified
Mathlib/CategoryTheory/DifferentialObject.lean
Modified
Mathlib/CategoryTheory/IsConnected.lean
Modified
Mathlib/CategoryTheory/Limits/Cones.lean
Modified
Mathlib/CategoryTheory/Limits/Final.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Images.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
Modified
Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean
Modified
Mathlib/CategoryTheory/Pi/Basic.lean
Modified
Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean
Modified
Mathlib/CategoryTheory/Preadditive/Mat.lean
Modified
Mathlib/CategoryTheory/Shift/Basic.lean
Modified
Mathlib/CategoryTheory/Sites/Canonical.lean
Modified
Mathlib/CategoryTheory/Sites/LeftExact.lean
Modified
Mathlib/CategoryTheory/Sites/Plus.lean
Modified
Mathlib/CategoryTheory/Sites/Sheaf.lean
Modified
Mathlib/Combinatorics/Additive/Behrend.lean
Modified
Mathlib/Combinatorics/Configuration.lean
Modified
Mathlib/Combinatorics/Hall/Finite.lean
Modified
Mathlib/Combinatorics/Quiver/Cast.lean
Modified
Mathlib/Combinatorics/SetFamily/Compression/UV.lean
Modified
Mathlib/Computability/DFA.lean
Modified
Mathlib/Computability/Halting.lean
Modified
Mathlib/Computability/RegularExpressions.lean
Modified
Mathlib/Computability/TuringMachine.lean
Modified
Mathlib/Data/Fin/Basic.lean
Modified
Mathlib/Data/Fin/VecNotation.lean
Modified
Mathlib/Data/List/OfFn.lean
Modified
Mathlib/Data/List/Pairwise.lean
Modified
Mathlib/Data/List/Perm.lean
Modified
Mathlib/Data/List/Sublists.lean
Modified
Mathlib/Data/Nat/Choose/Multinomial.lean
Modified
Mathlib/Data/Nat/Squarefree.lean
Modified
Mathlib/Data/PFun.lean
Modified
Mathlib/Data/PFunctor/Multivariate/W.lean
Modified
Mathlib/Data/PNat/Factors.lean
Modified
Mathlib/Data/PNat/Prime.lean
Modified
Mathlib/Data/Polynomial/Degree/Lemmas.lean
Modified
Mathlib/Data/Polynomial/UnitTrinomial.lean
Modified
Mathlib/Data/QPF/Multivariate/Basic.lean
Modified
Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
Modified
Mathlib/Data/QPF/Univariate/Basic.lean
Modified
Mathlib/Data/Rat/Star.lean
Modified
Mathlib/Data/Seq/Parallel.lean
Modified
Mathlib/Data/Seq/Seq.lean
Modified
Mathlib/Data/Set/Card.lean
Modified
Mathlib/Data/Stream/Init.lean
Modified
Mathlib/FieldTheory/PolynomialGaloisGroup.lean
Modified
Mathlib/Geometry/Euclidean/Circumcenter.lean
Modified
Mathlib/Geometry/Manifold/Instances/Real.lean
Modified
Mathlib/GroupTheory/SchurZassenhaus.lean
Modified
Mathlib/GroupTheory/Transfer.lean
Modified
Mathlib/Init/Data/Nat/Lemmas.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Independent.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean
Modified
Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
Modified
Mathlib/LinearAlgebra/Dual.lean
Modified
Mathlib/LinearAlgebra/Lagrange.lean
Modified
Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
Modified
Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean
Modified
Mathlib/LinearAlgebra/TensorPower.lean
Modified
Mathlib/Logic/Equiv/Embedding.lean
Modified
Mathlib/MeasureTheory/Constructions/Pi.lean
Modified
Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
Modified
Mathlib/MeasureTheory/Decomposition/UnsignedHahn.lean
Modified
Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
Modified
Mathlib/MeasureTheory/Function/LpSpace.lean
Modified
Mathlib/MeasureTheory/Integral/Average.lean
Modified
Mathlib/MeasureTheory/Integral/Bochner.lean
Modified
Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
Modified
Mathlib/MeasureTheory/Integral/Lebesgue.lean
Modified
Mathlib/MeasureTheory/Integral/SetToL1.lean
Modified
Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean
Modified
Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
Modified
Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
Modified
Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
Modified
Mathlib/MeasureTheory/PiSystem.lean
Modified
Mathlib/ModelTheory/Semantics.lean
Modified
Mathlib/NumberTheory/ADEInequality.lean
Modified
Mathlib/NumberTheory/ArithmeticFunction.lean
Modified
Mathlib/NumberTheory/Bernoulli.lean
Modified
Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean
Modified
Mathlib/NumberTheory/NumberField/Embeddings.lean
Modified
Mathlib/NumberTheory/Padics/PadicIntegers.lean
Modified
Mathlib/NumberTheory/Padics/RingHoms.lean
Modified
Mathlib/NumberTheory/ZetaFunction.lean
Modified
Mathlib/NumberTheory/ZetaValues.lean
Modified
Mathlib/Order/RelIso/Basic.lean
Modified
Mathlib/Order/WellFoundedSet.lean
Modified
Mathlib/Probability/Kernel/CondCdf.lean
Modified
Mathlib/Probability/Kernel/MeasurableIntegral.lean
Modified
Mathlib/Probability/Martingale/BorelCantelli.lean
Modified
Mathlib/Probability/ProbabilityMassFunction/Uniform.lean
Modified
Mathlib/Probability/Process/Filtration.lean
Modified
Mathlib/Probability/Variance.lean
Modified
Mathlib/RepresentationTheory/Basic.lean
Modified
Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
Modified
Mathlib/RingTheory/Coprime/Lemmas.lean
Modified
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
Modified
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
Modified
Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
Modified
Mathlib/RingTheory/Ideal/Operations.lean
Modified
Mathlib/RingTheory/MvPolynomial/Symmetric.lean
Modified
Mathlib/RingTheory/Norm.lean
Modified
Mathlib/RingTheory/OreLocalization/Basic.lean
Modified
Mathlib/RingTheory/Polynomial/Basic.lean
Modified
Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
Modified
Mathlib/RingTheory/Polynomial/Pochhammer.lean
Modified
Mathlib/RingTheory/PowerBasis.lean
Modified
Mathlib/RingTheory/RootsOfUnity/Minpoly.lean
Modified
Mathlib/RingTheory/Valuation/ValuationSubring.lean
Modified
Mathlib/RingTheory/WittVector/MulCoeff.lean
Modified
Mathlib/SetTheory/Game/Basic.lean
Modified
Mathlib/SetTheory/Ordinal/Notation.lean
Modified
Mathlib/SetTheory/Surreal/Dyadic.lean
Modified
Mathlib/Topology/Algebra/Semigroup.lean
Modified
Mathlib/Topology/Algebra/Valuation.lean
Modified
Mathlib/Topology/Algebra/ValuedField.lean
Modified
Mathlib/Topology/Category/TopCat/Limits/Products.lean
Modified
Mathlib/Topology/ContinuousFunction/Ideals.lean
Modified
Mathlib/Topology/Gluing.lean
Modified
Mathlib/Topology/Instances/AddCircle.lean
Modified
Mathlib/Topology/List.lean
Modified
Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean
Modified
Mathlib/Topology/Spectral/Hom.lean
Modified
test/Simps.lean
Modified
test/says.lean
Modified
test/solve_by_elim/basic.lean