Changelog

feat(ring_theory/mv_polynomial/ideal): lemmas about monomial ideals (#18633) …

feat(representation_theory/Rep): describe monoidal closed structure (#18148) …

chore(number_theory/pell): Move def. of solution type and API to beginning (#18639) …

feat(order/antichain): Antichains are order-connected (#18636)

chore(*): golf using `acc_lift₂_iff` and `well_founded_lift₂_iff` (#18526)

chore(set_theory/game/pgame): golf le and lf basic API (#18498)

chore(*): add mathlib4 synchronization comments (#18634) …

feat(algebra/monoid_algebra): add division by a generator (#15905) …

chore(*): add mathlib4 synchronization comments (#18630) …

chore(analysis/calculus/cont_diff): split into two files (#18627) …

chore(*): add mathlib4 synchronization comments (#18625) …

feat(analysis/calculus/cont_diff): formula for iterated derivative of composition with linear maps (#18592) …

chore(*): add mathlib4 synchronization comments (#18623) …

feat(data/matrix/kronecker): lemmas about trace, det, and inv (#18610) …

refactor(linear_algebra/matrix/hermitian): golf and generalize (#18565) …

feat(number_theory/pell): group structure (#18568) …

chore(linear_algebra/affine_space/affine_subspace) add set_like instance (#18622) …

chore(analysis/inner_product_space/basic): explicit `𝕜` argument for `innerₛₗ` and `innerSL` (#18613) …

chore(*): add mathlib4 synchronization comments (#18621) …

feat(algebra/group/commute): `div` lemmas (#18607) …

chore(linear_algebra/free_module/basic): golf a proof (#18615) …

perf(group_theory/torsion): Speedup `torsion_mul_equiv` (#18614) …

chore(topology/algebra/module/basic): move a lemma to a new file (#18608) …

chore(geometry/euclidean/sphere/basic): generalize typeclasses (#18605) …

chore(*): add mathlib4 synchronization comments (#18595) …

feat(algebra/quadratic_discriminant): generalize, use `ne_zero` (#18606) …

feat(data/set/sups): Set family operations (#18172) …

feat(algebra/*/opposite): Missing instances (#18602) …

chore (data/finset/sym): remove unnecessary alias (#18603) …

fix(analysis/inner_product_space/pi_L2): add missing type cast functions (#18574) …

chore(topology/basic): backport a generalization to Sort (#18544) …

chore(data/fintype/fin): add Iio lemmas (#18600) …

chore(ring_theory/power_series/basic): remove commutativity assumption (#18599) …

chore(algebra): generalize typeclass arguments from field to semifield (#18597) …

chore(algebra/ring/ulift): Split off and golf field instances (#18590) …

feat(analysis/normed_space/quaternion_exponential): lemmas about the quaternion exponential (#18349) …

chore(data/{nat,int}/cast/field): generalize to division_ring (#18598) …

feat(number_theory/modular_forms): Jacobi theta function (#18564) …

feat(analysis/inner_product_space/projection): express `orthogonal_projection` using `linear_proj_of_is_compl` (#18243) …

chore(algebra/order/nonneg/*): Separate `floor_ring` from `field` (#18596) …

chore(algebra/order/field/basic): Rename `pow_minus_two_nonneg` (#18591) …

refactor(geometry/euclidean): split out spheres (#18220) …

chore(data/mv_polynomial): reverse an import (#18593) …

feat(probability/kernel/invariance): Define pushforward of measure along a kernel (#18244)

feat(algebra/triv_sq_zero_ext): lemmas about big operators (#18488) …

chore(analysis/inner_product_space/basic): add inner_self_ne_zero (#18587) …

refactor(topology/algebra/open_subgroup): use `set_like` (#18585)

feat(analysis/normed/order/upper_lower): Thickening an upper set (#17257) …

chore(geometry/manifold/instances/sphere): speedup a proof (#18586) …

chore(order/with_bot): lemmas about unbot and untop (#18582)