Changelog

chore(Analysis/Normed/Lp/WithLp): generalize action-related instances on `WithLp` (#22706) …

chore(Algebra/Group/Basic): rename mul_right_eq_self to mul_eq_left etc (#22587) …

feat(Interval/Set/Fin): new file (#22452)

feat(NumberField/MixedSpace): add polar coordinates change of variables (part 2) (#22115) …

chore: review of porting notes in `CategoryTheory/` (#22899) …

refactor: change `⟪x, y⟫_𝕜 := conj x * y` to `y * conj x`. (#22715) …

chore: move Data.Set.Pointwise.Iterate to Dynamics.FixedPoints.Prufer (#22897) …

chore: move Equiv.Perm.viaFintypeEmbedding_sign out of Logic/ (#22900) …

refactor: add a `ContinuousSqrt` class to conclude `StarOrderedRing C(α, R)` (#18102)

feat: `lintegral_piecewise` (#22886) …

feat(MeasureTheory/Integral/Prod): add swap lemmas (#22401)

feat(RingTheory/DividedPowers/DPMorphism): add divided power morphisms (#22318) …

feat(List/Pairwise): add `rel_getLast` (#22427) …

chore(CategoryTheory/Closed/Cartesian): make cartesian closed categories computable (#22896) …

chore: review of porting notes in `Order/` (#22895)

chore(Data/Fintype): process porting notes (#22876) …

feat(CategoryTheory/WithTerminal): functors out of `WithTerminal` (#22658) …

feat: add to `WithVal` API (#22491) …

feat(LinearAlgebra/AffineSpace/Independent): interior of a simplex (#21929) …

chore (Analysis/Normed): rename `norm_mul` to `norm_mul_le` (#22871) …

feat(RingTheory/Ideal): more lemmas about the height of an ideal (#21041) …

feat: definitions for Tannaka duality for finite groups (#22173) …

feat(Finpartition): add constructor using existsUnique (#22807)

feat(Order/Atoms): generalise IsAtomistic typeclass assumptions (#22891) …

feat(Data/Nat/GCD/Basic): Prove `gcd (a ^ b - 1) (a ^ c - 1) = a ^ gcd b c - 1` (#22889) …

feat: comaps of subgroups and submonoids agree (#22873) …

chore(*): fix some to_additive-generated names (#22836) …

feat: improve definition of `AffineSubspace.mk'`, and use it in `perpBisector` (#22862) …

chore: review of porting notes in Analysis/ (#22773)

chore: update the neovim link in the Dockerfile (#21653) …

chore: whitespace again (#22878) …

chore(Data/(E)(NN)Real): address porting notes (#22883) …

chore(Data/(D)Finsupp): clean up porting notes (#22879) …

chore: upstream `OptionT` lemmas to batteries (#22859) …

ci: put cache cleanup step after lean is installed (#22887) …

fix(Group/Pointwise): fix some lemmas (#22729) …

feat(Logic/Equiv/Fin): add `finRotate` lemma (#22251)

ci: run lake exe cache clean if cache is larger than 10 GB (#22863) …

fix(CI): adapt to new olean path (#22506) …

chore(whitespace): more whitespace changes (#22850) …

feat(Counterexamples): disproof of the Aharoni–Korman conjecture (#20082) …

chore(whitespace): yet some more whitespace changes (#22854) …

chore(Data/List): address most porting notes (#22830) …

chore: resolve checkType porting note (#22711)

feat: density of a union of finsets (#22629) …

chore(Data/Finset): process porting notes (#22839) …

chore(Data/Multiset): clean up porting notes (#22835) …

chore(*): classify porting notes about delta derive handler (#22869) …

feat(Data/Nat/Find): Nat.find_mono_of_le and Nat.find_congr (#22811) …

chore(whitespace): some more changes in whitespace (#22840) …