Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-12-30 21:45
3694e27d
View on Github →
chore(*): drop
$
/
<|
before
fun
(
#9361
) Subset of
#9319
Estimated changes
Modified
Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
Modified
Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
Modified
Mathlib/Algebra/Associated.lean
Modified
Mathlib/Algebra/BigOperators/Associated.lean
Modified
Mathlib/Algebra/BigOperators/Basic.lean
Modified
Mathlib/Algebra/Category/GroupCat/Colimits.lean
Modified
Mathlib/Algebra/Category/GroupCat/Kernels.lean
Modified
Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
Modified
Mathlib/Algebra/Category/MonCat/Colimits.lean
Modified
Mathlib/Algebra/Category/Ring/Colimits.lean
Modified
Mathlib/Algebra/GCDMonoid/Finset.lean
Modified
Mathlib/Algebra/GCDMonoid/Multiset.lean
Modified
Mathlib/Algebra/GradedMonoid.lean
Modified
Mathlib/Algebra/Group/Equiv/Basic.lean
Modified
Mathlib/Algebra/Group/Pi.lean
Modified
Mathlib/Algebra/GroupWithZero/Basic.lean
Modified
Mathlib/Algebra/GroupWithZero/InjSurj.lean
Modified
Mathlib/Algebra/Module/Submodule/Pointwise.lean
Modified
Mathlib/Algebra/MonoidAlgebra/Basic.lean
Modified
Mathlib/Algebra/Order/Module/OrderedSMul.lean
Modified
Mathlib/Algebra/Order/Monovary.lean
Modified
Mathlib/Algebra/Order/Ring/WithTop.lean
Modified
Mathlib/Algebra/Ring/CentroidHom.lean
Modified
Mathlib/Algebra/RingQuot.lean
Modified
Mathlib/Algebra/SMulWithZero.lean
modified
theorem
left_ne_zero_of_smul
Modified
Mathlib/AlgebraicTopology/SimplexCategory.lean
Modified
Mathlib/AlgebraicTopology/SimplicialObject.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/Basic.lean
Modified
Mathlib/Analysis/Calculus/MeanValue.lean
Modified
Mathlib/Analysis/Complex/CauchyIntegral.lean
Modified
Mathlib/Analysis/Matrix.lean
Modified
Mathlib/Analysis/Normed/Field/InfiniteSum.lean
Modified
Mathlib/Analysis/SpecialFunctions/Bernstein.lean
Modified
Mathlib/CategoryTheory/Extensive.lean
Modified
Mathlib/CategoryTheory/Limits/VanKampen.lean
Modified
Mathlib/CategoryTheory/PathCategory.lean
Modified
Mathlib/Combinatorics/Partition.lean
Modified
Mathlib/Combinatorics/Pigeonhole.lean
Modified
Mathlib/Combinatorics/SetFamily/FourFunctions.lean
modified
theorem
collapse_nonneg
Modified
Mathlib/Combinatorics/SetFamily/Shatter.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Basic.lean
Modified
Mathlib/Computability/AkraBazzi/AkraBazzi.lean
Modified
Mathlib/Computability/Primrec.lean
Modified
Mathlib/Control/EquivFunctor.lean
Modified
Mathlib/Control/Functor.lean
Modified
Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean
Modified
Mathlib/Data/Finmap.lean
Modified
Mathlib/Data/Finset/Basic.lean
Modified
Mathlib/Data/Finset/Powerset.lean
Modified
Mathlib/Data/Finsupp/Multiset.lean
Modified
Mathlib/Data/Fintype/Basic.lean
Modified
Mathlib/Data/Fintype/Pi.lean
Modified
Mathlib/Data/FunLike/Equiv.lean
Modified
Mathlib/Data/List/Defs.lean
Modified
Mathlib/Data/List/Forall2.lean
Modified
Mathlib/Data/List/Prime.lean
Modified
Mathlib/Data/List/Sublists.lean
Modified
Mathlib/Data/Matrix/Basic.lean
Modified
Mathlib/Data/Matroid/Basic.lean
Modified
Mathlib/Data/Matroid/IndepAxioms.lean
Modified
Mathlib/Data/Multiset/Antidiagonal.lean
Modified
Mathlib/Data/Multiset/Basic.lean
Modified
Mathlib/Data/Multiset/Nodup.lean
Modified
Mathlib/Data/Nat/Digits.lean
Modified
Mathlib/Data/PFun.lean
Modified
Mathlib/Data/Real/CauSeq.lean
Modified
Mathlib/Data/Real/EReal.lean
Modified
Mathlib/Data/Real/Hyperreal.lean
Modified
Mathlib/Data/Semiquot.lean
Modified
Mathlib/Data/Set/Basic.lean
Modified
Mathlib/Data/Set/Finite.lean
Modified
Mathlib/Data/Set/Function.lean
Modified
Mathlib/Data/Set/Lattice.lean
Modified
Mathlib/Data/Set/List.lean
Modified
Mathlib/Data/Set/Prod.lean
Modified
Mathlib/Data/Sigma/Lex.lean
Modified
Mathlib/Data/TypeVec.lean
Modified
Mathlib/FieldTheory/Fixed.lean
Modified
Mathlib/FieldTheory/IsSepClosed.lean
Modified
Mathlib/FieldTheory/Perfect.lean
Modified
Mathlib/FieldTheory/SeparableDegree.lean
Modified
Mathlib/Geometry/Euclidean/Inversion/ImageHyperplane.lean
Modified
Mathlib/Geometry/Euclidean/PerpBisector.lean
Modified
Mathlib/GroupTheory/Congruence.lean
Modified
Mathlib/GroupTheory/GroupAction/DomAct/Basic.lean
Modified
Mathlib/GroupTheory/OrderOfElement.lean
Modified
Mathlib/GroupTheory/Perm/Basic.lean
Modified
Mathlib/GroupTheory/PushoutI.lean
Modified
Mathlib/GroupTheory/Transfer.lean
Modified
Mathlib/Init/Data/List/Instances.lean
Modified
Mathlib/Lean/Expr/Traverse.lean
Modified
Mathlib/LinearAlgebra/BilinearForm/Basic.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
Modified
Mathlib/LinearAlgebra/DFinsupp.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Basic.lean
Modified
Mathlib/LinearAlgebra/InvariantBasisNumber.lean
Modified
Mathlib/LinearAlgebra/Matrix/PosDef.lean
Modified
Mathlib/LinearAlgebra/Matrix/Spectrum.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
Modified
Mathlib/LinearAlgebra/TensorAlgebra/Basis.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
Modified
Mathlib/LinearAlgebra/TensorProduct/Tower.lean
Modified
Mathlib/Logic/Function/Basic.lean
Modified
Mathlib/Logic/Relator.lean
Modified
Mathlib/Mathport/Notation.lean
Modified
Mathlib/MeasureTheory/Function/AEEqFun.lean
Modified
Mathlib/MeasureTheory/Function/LpSpace.lean
Modified
Mathlib/MeasureTheory/Group/Measure.lean
Modified
Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
Modified
Mathlib/MeasureTheory/Integral/MeanInequalities.lean
Modified
Mathlib/NumberTheory/BernoulliPolynomials.lean
Modified
Mathlib/NumberTheory/NumberField/Embeddings.lean
Modified
Mathlib/NumberTheory/Padics/PadicNumbers.lean
Modified
Mathlib/NumberTheory/SmoothNumbers.lean
Modified
Mathlib/NumberTheory/SumPrimeReciprocals.lean
Modified
Mathlib/Order/Closure.lean
Modified
Mathlib/Order/CompleteLattice.lean
Modified
Mathlib/Order/Filter/Bases.lean
Modified
Mathlib/Order/Filter/Basic.lean
Modified
Mathlib/Order/Filter/Germ.lean
Modified
Mathlib/Order/Iterate.lean
Modified
Mathlib/Order/Lattice.lean
Modified
Mathlib/Order/Minimal.lean
Modified
Mathlib/Order/OmegaCompletePartialOrder.lean
Modified
Mathlib/Order/RelSeries.lean
Modified
Mathlib/Order/Sublattice.lean
Modified
Mathlib/Order/SupClosed.lean
Modified
Mathlib/Order/WellFoundedSet.lean
Modified
Mathlib/Probability/Kernel/Basic.lean
Modified
Mathlib/Probability/Kernel/Disintegration.lean
Modified
Mathlib/RepresentationTheory/GroupCohomology/Hilbert90.lean
Modified
Mathlib/RingTheory/DedekindDomain/Different.lean
Modified
Mathlib/RingTheory/TensorProduct.lean
Modified
Mathlib/SetTheory/Game/PGame.lean
Modified
Mathlib/Tactic/ApplyCongr.lean
Modified
Mathlib/Tactic/Linarith/Datatypes.lean
Modified
Mathlib/Tactic/Linarith/Elimination.lean
Modified
Mathlib/Tactic/Linarith/Parsing.lean
Modified
Mathlib/Tactic/Linarith/Preprocessing.lean
Modified
Mathlib/Tactic/ReduceModChar.lean
Modified
Mathlib/Tactic/ToAdditive.lean
Modified
Mathlib/Tactic/WLOG.lean
Modified
Mathlib/Testing/SlimCheck/Functions.lean
Modified
Mathlib/Testing/SlimCheck/Testable.lean
Modified
Mathlib/Topology/AlexandrovDiscrete.lean
modified
theorem
subset_exterior
Modified
Mathlib/Topology/Algebra/GroupWithZero.lean
Modified
Mathlib/Topology/Algebra/Order/Compact.lean
Modified
Mathlib/Topology/Algebra/Order/Floor.lean
Modified
Mathlib/Topology/Algebra/UniformGroup.lean
Modified
Mathlib/Topology/Basic.lean
Modified
Mathlib/Topology/Category/TopCat/Limits/Basic.lean
Modified
Mathlib/Topology/Compactness/Compact.lean
Modified
Mathlib/Topology/Connected/LocallyConnected.lean
Modified
Mathlib/Topology/Constructions.lean
Modified
Mathlib/Topology/ContinuousOn.lean
Modified
Mathlib/Topology/EMetricSpace/Basic.lean
Modified
Mathlib/Topology/Homeomorph.lean
Modified
Mathlib/Topology/LocallyConstant/Basic.lean
Modified
Mathlib/Topology/MetricSpace/Algebra.lean
Modified
Mathlib/Topology/MetricSpace/Basic.lean
Modified
Mathlib/Topology/MetricSpace/Dilation.lean
Modified
Mathlib/Topology/NoetherianSpace.lean
Modified
Mathlib/Topology/Order/ScottTopology.lean
Modified
Mathlib/Topology/PartialHomeomorph.lean
Modified
Mathlib/Topology/UniformSpace/Basic.lean
Modified
Mathlib/Topology/UniformSpace/Equiv.lean
Modified
Mathlib/Topology/UniformSpace/UniformConvergence.lean
Modified
Mathlib/Util/Delaborators.lean
Modified
test/Traversable.lean