Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-01-21 18:51
590c3a6d
View on Github →
chore: review of
nolint simpNF
(
#20867
) Closes
#18942
.
Estimated changes
Modified
Mathlib/Algebra/Category/Semigrp/Basic.lean
Modified
Mathlib/Algebra/Free.lean
Modified
Mathlib/Algebra/Homology/DifferentialObject.lean
Modified
Mathlib/Algebra/Order/CompleteField.lean
Modified
Mathlib/Algebra/Ring/Commute.lean
Modified
Mathlib/Algebra/Ring/Subring/Basic.lean
Modified
Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
Modified
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean
Modified
Mathlib/AlgebraicGeometry/Spec.lean
Modified
Mathlib/AlgebraicGeometry/StructureSheaf.lean
Modified
Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean
Modified
Mathlib/Analysis/CStarAlgebra/Basic.lean
Modified
Mathlib/Analysis/Normed/Group/Hom.lean
Modified
Mathlib/Analysis/Normed/Group/SemiNormedGrp/Completion.lean
Modified
Mathlib/Analysis/Normed/Group/Seminorm.lean
Modified
Mathlib/Analysis/VonNeumannAlgebra/Basic.lean
Modified
Mathlib/CategoryTheory/Action/Monoidal.lean
Modified
Mathlib/CategoryTheory/Closed/Cartesian.lean
Modified
Mathlib/CategoryTheory/Closed/FunctorCategory/Groupoid.lean
Modified
Mathlib/CategoryTheory/Comma/Over.lean
Modified
Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
deleted
theorem
CategoryTheory.Limits.WalkingParallelPairHom.id.sizeOf_spec'
Modified
Mathlib/CategoryTheory/Limits/Shapes/Images.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
Modified
Mathlib/CategoryTheory/Monoidal/Free/Basic.lean
Modified
Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.lean
Modified
Mathlib/CategoryTheory/Sites/Sheaf.lean
Modified
Mathlib/CategoryTheory/Subobject/Comma.lean
Modified
Mathlib/Data/DFinsupp/BigOperators.lean
Modified
Mathlib/Data/DFinsupp/Defs.lean
Modified
Mathlib/Data/Fin/Tuple/Basic.lean
Modified
Mathlib/Data/Finset/Lattice/Fold.lean
Modified
Mathlib/Data/Finset/Sups.lean
Modified
Mathlib/Data/Finset/Sym.lean
Modified
Mathlib/Data/Finset/Union.lean
modified
theorem
Finset.disjiUnion_filter_eq
Modified
Mathlib/Data/Finsupp/Basic.lean
Modified
Mathlib/Data/Finsupp/ToDFinsupp.lean
Modified
Mathlib/Data/List/Basic.lean
Modified
Mathlib/Data/Matrix/DMatrix.lean
Modified
Mathlib/Data/Matrix/Defs.lean
Modified
Mathlib/Data/Matrix/Diagonal.lean
Modified
Mathlib/Data/Matrix/Mul.lean
Modified
Mathlib/Data/NNRat/Defs.lean
Modified
Mathlib/Data/Set/Function.lean
Modified
Mathlib/Data/Set/MulAntidiagonal.lean
Modified
Mathlib/Data/SetLike/Basic.lean
Modified
Mathlib/Data/Setoid/Partition.lean
Modified
Mathlib/Data/Sigma/Basic.lean
Modified
Mathlib/Data/Sign.lean
Modified
Mathlib/Data/Subtype.lean
Modified
Mathlib/FieldTheory/IntermediateField/Basic.lean
Modified
Mathlib/Geometry/Manifold/ChartedSpace.lean
Modified
Mathlib/GroupTheory/Complement.lean
Modified
Mathlib/GroupTheory/OrderOfElement.lean
Modified
Mathlib/GroupTheory/SemidirectProduct.lean
Modified
Mathlib/LinearAlgebra/Isomorphisms.lean
Modified
Mathlib/LinearAlgebra/Matrix/ToLin.lean
Modified
Mathlib/LinearAlgebra/Multilinear/Basic.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
Modified
Mathlib/Logic/Unique.lean
Modified
Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
Modified
Mathlib/NumberTheory/Divisors.lean
Modified
Mathlib/Order/Category/BddLat.lean
Modified
Mathlib/Order/Interval/Basic.lean
Modified
Mathlib/Topology/Algebra/Module/Star.lean
Modified
Mathlib/Topology/Category/LightProfinite/Basic.lean
Modified
Mathlib/Topology/Category/Profinite/Basic.lean
Modified
Mathlib/Topology/ContinuousMap/Units.lean