Changelog

chore: robustifying for debug.byAsSorry (part 5) (#15126)

chore: robustifying for debug.byAsSorry (part 4) (#15125)

chore: split `Topology.Connected.Basic` (#15144) …

chore: enable workflow_dispatch for nightly_bump_toolchain (#15143)

chore: bump nightly toolchain more often (#15142)

Chore: robustifying for debug.byAsSorry (part 7) (#15137) …

chore: more adaptations for debugAsSorry (#15133)

feat(AlgebraicGeometry): Define affine morphisms (#13996)

feat: the long line linter as a syntax linter (#15097) …

feat: new file `Data/List/Pi` (#5549) …

chore: make `#where` command commonly available again (#15139)

refactor(CategoryTheory/Sites): Allow non-fully-faithful dense subsites. (#15056)

chore: update Mathlib dependencies 2024-07-25 (#15138) …

doc(BigOperators): Expand `Finset.sum` docstring (#15134) …

feat(Analysis/Complex): If `a = ∑ i ∈ s, f i` and `b = ∑ i ∈ s, (‖f i‖ : ℂ)`, then `a ≤ b` (#15022) …

fix: `aesop_graph?` macro (#15124) …

feat(Group/Measure): drop a `MeasurableMul` assumption (#15041) …

chore: robustifying for debug.byAsSorry (part 3) (#15120) …

chore: robustifying for debug.byAsSorry (part 2) (#15119) …

feat(Ergodic/Conservative): generalize to `NullMeasurableSet`s (#15086) …

chore: deprecate `sizeOf_dropSlice_lt` (#15118) …

feat: generalize constant 5 in Vitali covering (#15117) …

Feat(RingTheory/Flat): add localization of flat module is flat (#15023) …

chore(Algebra/Order/GroupWithZero/Unbundled): resolving name inconsistencies (#9904) …

feat(Topology/Sequences): preservation of sequential compactness under continuous functions (#14504) …

chore(Tactic/CategoryTheory/Coherence): import non-meta coherence theorem (#15067) …

feat(Data/Set/Basic, Order/RelClasses): add @[simp] to subset_refl and subset_empty_iff (#15110) …

chore: long lines in tests (#15111) …

feat(RingTheory/Idempotents): Lifting complete orthogonal idempotents along nil extensions (#14372)

chore: protect `congr_arg`'s and `congr_fun`'s (#15083) …

fix(Tactic/Simps): Prevent `simps` from viewing `field_1` as a prefix of `field`. (#15095) …

style: whitespace and long line (#15107) …

feat(RingTheory.MvPolynomial.WeightedHomogeneous): add graded algebra structure (#14225) …

chore: move `PartialOrder` on `PrimeSpectrum` to `RingTheory`. (#15108)

perf(PiTensorProduct/InjectiveSeminorm): squeeze slow simp (#15102) …

chore: fix some non-flexible simps (#15101) …

fix: shorten lines with 101 characters (#15104) …

chore(Kernel/Disintegration): Rename `Basic` to `StandardBorel` (#15103) …

fix: parse header in `minImports` to improve reports (#15081) …

feat: the Galois connection induced by an arbitrary relation (#14908) …

feat(ZMod): Simple lemmas (#15076) …

chore: address `elab_as_elim` workarounds (#15091) …

refactor(RingTheory/Trace/Basic): remove `Field` assumptions (#15039) …

feat(Archive/Imo): IMO 2024 Q2 (#14920) …

feat (Algebra/Ring): add `isSemireal` class for commutative rings (#14941) …

feat(CategoryTheory/Site): Locally fully-faithful functors into sites. (#15062)

feat(RingTheory): being finitely-presented is local (#15073)

feat(Pullback/CommSq): add more pasting lemmas for `IsPullback` (#14985) …

feat(MeasureSpace): generalize pigeonhole to NullMeasurableSets (#15089)

feat(ContinuousMapDense): weaken TC assumptions (#15085) …