Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-02-02 04:48
490d2d48
View on Github →
chore: move to v4.6.0-rc1, merging adaptations from bump/v4.6.0 (
#10176
)
Estimated changes
Modified
.github/workflows/bors.yml
Modified
.github/workflows/build.yml
Modified
.github/workflows/build.yml.in
Modified
.github/workflows/build_fork.yml
Modified
Archive/Examples/IfNormalization/Result.lean
Modified
Archive/Examples/IfNormalization/WithoutAesop.lean
Modified
Archive/Wiedijk100Theorems/BallotProblem.lean
Modified
Counterexamples/CharPZeroNeCharZero.lean
Modified
Mathlib/Algebra/Category/GroupCat/Basic.lean
Modified
Mathlib/Algebra/DirectLimit.lean
Modified
Mathlib/Algebra/DirectSum/Basic.lean
Modified
Mathlib/Algebra/EuclideanDomain/Defs.lean
Modified
Mathlib/Algebra/GCDMonoid/Basic.lean
Modified
Mathlib/Algebra/Group/Basic.lean
Modified
Mathlib/Algebra/Group/Equiv/TypeTags.lean
modified
def
addMonoidEndToMultiplicative
modified
def
monoidEndToAdditive
Modified
Mathlib/Algebra/Group/WithOne/Defs.lean
Modified
Mathlib/Algebra/Lie/Abelian.lean
Modified
Mathlib/Algebra/Lie/DirectSum.lean
Modified
Mathlib/Algebra/Lie/Subalgebra.lean
Modified
Mathlib/Algebra/Lie/Submodule.lean
Modified
Mathlib/Algebra/Lie/Weights/Linear.lean
Modified
Mathlib/Algebra/Module/Injective.lean
Modified
Mathlib/Algebra/Order/WithZero.lean
Modified
Mathlib/Algebra/Ring/BooleanRing.lean
Modified
Mathlib/Algebra/Ring/Idempotents.lean
modified
theorem
IsIdempotentElem.of_isIdempotent
Modified
Mathlib/Algebra/Ring/Pi.lean
Modified
Mathlib/Analysis/Analytic/Composition.lean
Modified
Mathlib/Analysis/Fourier/AddCircle.lean
Modified
Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
Modified
Mathlib/Analysis/NormedSpace/AffineIsometry.lean
Modified
Mathlib/CategoryTheory/Monad/EquivMon.lean
Modified
Mathlib/CategoryTheory/Monoidal/Mod_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Preadditive.lean
Modified
Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean
Modified
Mathlib/CategoryTheory/Preadditive/OfBiproducts.lean
Modified
Mathlib/CategoryTheory/Sites/CoverPreserving.lean
Modified
Mathlib/Combinatorics/Catalan.lean
Modified
Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
Modified
Mathlib/Computability/Ackermann.lean
Modified
Mathlib/Computability/PartrecCode.lean
Modified
Mathlib/Computability/RegularExpressions.lean
Modified
Mathlib/Data/BinaryHeap.lean
Modified
Mathlib/Data/ByteArray.lean
Modified
Mathlib/Data/Finset/Basic.lean
Modified
Mathlib/Data/Finset/Card.lean
Modified
Mathlib/Data/Finset/Fold.lean
modified
theorem
Finset.fold_hom
modified
theorem
Finset.fold_image_idem
modified
theorem
Finset.fold_insert_idem
modified
theorem
Finset.fold_ite
Modified
Mathlib/Data/Finset/LocallyFinite.lean
Modified
Mathlib/Data/Finset/NoncommProd.lean
modified
theorem
Multiset.noncommFold_eq_fold
Modified
Mathlib/Data/Fintype/Basic.lean
Modified
Mathlib/Data/Fintype/Lattice.lean
Modified
Mathlib/Data/List/Basic.lean
Modified
Mathlib/Data/List/Defs.lean
Modified
Mathlib/Data/List/Infix.lean
Modified
Mathlib/Data/List/Perm.lean
Modified
Mathlib/Data/List/Sort.lean
Modified
Mathlib/Data/List/Sym.lean
Modified
Mathlib/Data/Matroid/Basic.lean
Modified
Mathlib/Data/Multiset/Basic.lean
Modified
Mathlib/Data/Multiset/Fold.lean
modified
theorem
Multiset.fold_dedup_idem
modified
theorem
Multiset.fold_hom
Modified
Mathlib/Data/MvPolynomial/Expand.lean
Modified
Mathlib/Data/Nat/Cast/Defs.lean
Modified
Mathlib/Data/Nat/Choose/Basic.lean
Modified
Mathlib/Data/Nat/Choose/Sum.lean
Modified
Mathlib/Data/Nat/Defs.lean
Modified
Mathlib/Data/Nat/Factorial/Basic.lean
Modified
Mathlib/Data/Nat/Hyperoperation.lean
Modified
Mathlib/Data/Nat/Order/Basic.lean
Modified
Mathlib/Data/Nat/Prime.lean
Modified
Mathlib/Data/Nat/Squarefree.lean
Modified
Mathlib/Data/Num/Prime.lean
Modified
Mathlib/Data/Option/Defs.lean
Modified
Mathlib/Data/Ordmap/Ordnode.lean
Modified
Mathlib/Data/PNat/Defs.lean
Modified
Mathlib/Data/Polynomial/Div.lean
Modified
Mathlib/Data/Polynomial/Inductions.lean
Modified
Mathlib/Data/Polynomial/Lifts.lean
Modified
Mathlib/Data/Polynomial/RingDivision.lean
Modified
Mathlib/Data/Prod/TProd.lean
Modified
Mathlib/Data/Set/Basic.lean
Modified
Mathlib/Data/Set/Card.lean
Modified
Mathlib/Data/Sym/Card.lean
Modified
Mathlib/Data/UnionFind.lean
Modified
Mathlib/Geometry/Euclidean/Circumcenter.lean
Modified
Mathlib/GroupTheory/CommutingProbability.lean
Modified
Mathlib/GroupTheory/EckmannHilton.lean
modified
structure
EckmannHilton.IsUnital
modified
theorem
EckmannHilton.mul_assoc
modified
theorem
EckmannHilton.mul_comm
Modified
Mathlib/GroupTheory/OrderOfElement.lean
Modified
Mathlib/GroupTheory/Perm/Basic.lean
Modified
Mathlib/GroupTheory/Perm/Cycle/Basic.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
Modified
Mathlib/GroupTheory/Subgroup/Basic.lean
Modified
Mathlib/Init/Algebra/Classes.lean
Modified
Mathlib/Lean/Meta/Simp.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
Modified
Mathlib/LinearAlgebra/Projectivization/Subspace.lean
Modified
Mathlib/Logic/Basic.lean
Modified
Mathlib/Logic/Equiv/Basic.lean
Modified
Mathlib/Logic/Function/Conjugate.lean
modified
theorem
Function.Semiconj₂.isAssociative_left
modified
theorem
Function.Semiconj₂.isAssociative_right
modified
theorem
Function.Semiconj₂.isIdempotent_left
modified
theorem
Function.Semiconj₂.isIdempotent_right
Modified
Mathlib/MeasureTheory/Covering/Besicovitch.lean
Modified
Mathlib/MeasureTheory/Integral/SetToL1.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/Card.lean
Modified
Mathlib/NumberTheory/SumFourSquares.lean
Modified
Mathlib/Order/Estimator.lean
Modified
Mathlib/Order/Lattice.lean
Modified
Mathlib/Order/MinMax.lean
modified
theorem
min_associative
Modified
Mathlib/Order/RelClasses.lean
Modified
Mathlib/Order/SymmDiff.lean
Modified
Mathlib/Probability/ProbabilityMassFunction/Monad.lean
Modified
Mathlib/Probability/Variance.lean
Modified
Mathlib/RepresentationTheory/GroupCohomology/Hilbert90.lean
Modified
Mathlib/RingTheory/DedekindDomain/Ideal.lean
Modified
Mathlib/RingTheory/HahnSeries.lean
Modified
Mathlib/RingTheory/Multiplicity.lean
Modified
Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
Modified
Mathlib/RingTheory/PowerSeries/Basic.lean
Modified
Mathlib/RingTheory/Valuation/ValuationSubring.lean
Modified
Mathlib/SetTheory/Game/Basic.lean
Modified
Mathlib/SetTheory/Game/Birthday.lean
Modified
Mathlib/SetTheory/Game/Impartial.lean
Modified
Mathlib/SetTheory/Game/Nim.lean
Modified
Mathlib/SetTheory/Game/Ordinal.lean
Modified
Mathlib/SetTheory/Game/PGame.lean
Modified
Mathlib/SetTheory/Game/Short.lean
Modified
Mathlib/SetTheory/Lists.lean
Modified
Mathlib/SetTheory/Ordinal/Basic.lean
Modified
Mathlib/SetTheory/Ordinal/CantorNormalForm.lean
Modified
Mathlib/SetTheory/Ordinal/NaturalOps.lean
Modified
Mathlib/SetTheory/Ordinal/Notation.lean
Modified
Mathlib/SetTheory/Surreal/Basic.lean
Modified
Mathlib/SetTheory/ZFC/Basic.lean
Modified
Mathlib/Tactic/Abel.lean
Modified
Mathlib/Tactic/Attr/Register.lean
Modified
Mathlib/Tactic/Cases.lean
Modified
Mathlib/Tactic/Core.lean
Modified
Mathlib/Tactic/DeriveTraversable.lean
modified
def
Mathlib.Deriving.Traversable.simpFunctorGoal
Modified
Mathlib/Tactic/FailIfNoProgress.lean
Modified
Mathlib/Tactic/FieldSimp.lean
Modified
Mathlib/Tactic/Lemma.lean
Modified
Mathlib/Tactic/NormNum/Core.lean
added
def
Mathlib.Meta.NormNum.tryNormNum
deleted
def
Mathlib.Meta.NormNum.tryNormNum?
Modified
Mathlib/Tactic/PPWithUniv.lean
Modified
Mathlib/Tactic/Positivity/Core.lean
Modified
Mathlib/Tactic/Propose.lean
Modified
Mathlib/Tactic/PushNeg.lean
Modified
Mathlib/Tactic/ReduceModChar.lean
Modified
Mathlib/Tactic/Relation/Trans.lean
Modified
Mathlib/Tactic/Rewrites.lean
Modified
Mathlib/Tactic/Ring/RingNF.lean
Modified
Mathlib/Tactic/SimpIntro.lean
Modified
Mathlib/Tactic/Simps/Basic.lean
Modified
Mathlib/Tactic/SplitIfs.lean
Modified
Mathlib/Tactic/SuppressCompilation.lean
Modified
Mathlib/Tactic/TFAE.lean
Modified
Mathlib/Testing/SlimCheck/Sampleable.lean
Modified
Mathlib/Topology/Homotopy/HomotopyGroup.lean
Modified
Mathlib/Util/AtomM.lean
Modified
Mathlib/Util/DischargerAsTactic.lean
Modified
lake-manifest.json
Modified
lakefile.lean
Modified
lean-toolchain
Modified
test/RewriteSearch/Basic.lean
Modified
test/delaborators.lean
Modified
test/matrix.lean