Changelog

feat(Data/Matrix): Equalities relating `mulVec` and `smul` (#12538) …

feat: exclude aesop from nonterminal simp check (#12585) …

chore(SimpleGraph/Regularity): Don't use `Classical` (#12575) …

chore: Rename `Dart.is_adj` to `Dart.adj` (#12574) …

chore: Rename `Finset.inter_sdiff` to `Finset.inter_sdiff_assoc` (#12573) …

chore: adaptations to lean 4.8.0 (#12583) …

feat: make `rank_mul_eq_left_of_isUnit_det` into an effective `simp` lemma (#12244) …

feat(RingTheory/AdicCompletion): refactor and expand API (#12516) …

feat(NumberTheory/DirichletCharacter): vanishing of Gauss sums when add char is imprimitive (#12324) …

feat(Algebra/Lie): existence of Cartan subalgebras (#12297)

chore: adaptations to lean 4.8.0 (#12578)

perf(AG.RingHomProperties): less defeq abuse (#12563) …

chore: missing `DecidableEq (DirectSum _ _)` instance (#12491)

feat(Order/Minimals, Order/RelIso/Set): four `RelIso` lemmas (#12558) …

chore: remove @[simp] from Fintype.card_fun (#12577) …

chore: update to leanprover/std4#769 (#12476)

chore: remove simp from Finset.filter_congr_decidable (#12576) …

refactor(Condensed): redefine condensed abelian groups as condensed `ℤ`-modules (#12510)

chore(CategoryTheory/MorphismProperty): Use le instead of subset (#12520)

feat: make `Fact` testable for `slim_check` (#12566) …

chore: update for leanprover/std4#758 (#12475)

feat: make multiplication in [Add]MonoidAlgebra irreducible (#12554) …

feat(CategoryTheory/Yoneda): dualize yoneda lemma (#12041) …

perf(AlgebraicGeometry.Spec): add explicit universe annotations (#12557) …

chore: adaptations to lean 4.8.0 (#12562)

feat: `{Mv}Polynomial.algebraMap_apply` simps (#11193) …

perf: make LocalInvariantProp a structure (#12552) …

chore: adaptations to lean 4.8.0 (#12549)

chore: move summable lemmas (#12503) …

feat(Algebra/Category/ModuleCat): the category of sheaves of modules has limits (#12269)

feat(Complex/UpperHalfPlane): add vertical strips (#12443) …

feat: `∑ x ∈ s, f x` to replace `∑ x in s, f x` in the future (#6795) …

chore(Init/Order/Defs): alias for le_antisymm (#12545)

chore: adapt to multiple goal linter 3 (#12372) …

perf(Computability/AkraBazzi): fix slow aesop call (#12541) …

feat(Rat): Numerator and denominator of `q ^ n` (#12506) …

feat(CategoryTheory): whiskering a fully faithful functor is full (#12527) …

chore(NumberField/Units): split into two files (#12509) …

chore: adapt to multiple goal linter 2 (#12361) …

chore(List): delete old, unused, deprecated theorems (#9607) …

chore: adapt to multiple goal linter 1 (#12338) …

feat: More big operator lemmas (#10551) …

chore: minor backports from nightly-testing (#12531)

chore: HahnSeries.ofPowerSeries_X_pow linter complains on nightly-testing (#12529) …

feat(RingTheory/Finiteness): relax the condition of `Module.Finite.exists_fin'` (#12524) …

docs: fix markdown link (#12512)

chore(AdicCompletion): move to `RingTheory` and make folder (#12511) …

feat(CategoryTheory/Triangulated): homological functors (#11759) …

fix: get `variable?` to handle `Type*` and `Sort*` (#8908) …

feat: `FastSubsingleton` and `FastIsEmpty` to speed up `congr!`/`convert` (#12495) …