leanprover-community/mathlib

Pull Requests Commits

chore(analysis/specific_limits/basic): generalize away from `ℝ`

eric-wieser committed 2 years ago

9d931dbd

chore(.github/workflows): update get-changed-files and download-artifact version (#18765)

alexjbest committed 2 years ago

86d04064

chore(.github/workflows): update checkout and setup python versions (#18764)

alexjbest committed 2 years ago

7cc39182

refactor(algebra/quaternion): remove `quaternion.conj` (#18803)

eric-wieser committed 2 years ago

cf7a7252

chore(*): add mathlib4 synchronization comments (#18889)

leanprover-community-bot committed 2 years ago

f2b757fc

chore(.github/workflows): replace set-output commands (#18762)

alexjbest committed 2 years ago

a4f99eae

chore(.github/workflows): update cancel workflow action (#18761)

alexjbest committed 2 years ago

eee67e6e

feat(algebra/group/basic): `a * b ≠ b ↔ a ≠ 1` (#18635)

YaelDillies committed 2 years ago

84771a9f

chore(data/finset/lattice): Remove `finset.sup_finset_image` (#18893)

YaelDillies committed 2 years ago

c813ed7d

feat(field_theory/tower): generalize `rank_mul_rank` to rings (#18885)

eric-wieser committed 2 years ago

c7bce281

chore(measure_theory/integral/lebesgue): generalize lintegral_sub and lintegral_sub_le to ae_measurable (#18883)

RemyDegenne committed 2 years ago

f231b9d8

feat(measure_theory/constructions/borel_space): add measurable_c{Inf/supr/infi} (#18882)

RemyDegenne committed 2 years ago

9c5398f2

chore(measure_theory/measure/haar_of_basis): axis-aligned parallepipeds are cuboids (#18829)

eric-wieser committed 2 years ago

ef093414

chore(category_theory/limits/preserves/finite): avoid instances with unbound universes (#18890)

kim-em committed 2 years ago

3974a774

fix(algebra/big_operators): add missing `to_additive`s (#18878)

eric-wieser committed 2 years ago

fa230957

chore(field_theory/tower): remove unneeded imports (#18891)

kim-em committed 2 years ago

f95ecd88

chore(topology/continuous_function/algebra): simplify definition and proof (#18888)

eric-wieser committed 2 years ago

16e59248

chore(data/matrix/block): the block matrix of zeros is zero (#18879)

eric-wieser committed 2 years ago

c060baa7

chore(mv_polynomial/funext): backport golfed proof (#18839)

kim-em committed 2 years ago

0b899341

chore(category_theory/abelian): backport removal of abelian.has_finite_biproducts instance (#18740)

kim-em committed 2 years ago

a5ff45a1

feat(ring_theory/polynomial): add properties of `coeff (hermite n)` (#18837)

lukemantle committed 2 years ago

b17e2720

chore(ring_theory/finiteness): generalize `module.finite.trans` (#18880)

eric-wieser committed 2 years ago

fa78268d

feat(linear_algebra/basis): add basis.restrict_scalars (#18814)

xroblot committed 2 years ago

04cdee31

chore(*): add mathlib4 synchronization comments (#18853)

leanprover-community-bot committed 2 years ago

9d2f0748

chore(finsupp/basic): weaken hypotheses (#18874)

ericrbg committed 2 years ago

57911c5a

feat(measure_theory/constructions): add the Borel isomorphism theorem. (#18864)

Felix-Weilacher committed 2 years ago

9b2b58d6

chore(algebra/star/basic): generalize quaternion lemmas (#18802)

eric-wieser committed 2 years ago

dc7ac07a

feat(algebra/big_operators/fin): The equivalence between `fin n → fin m` and `fin (m ^ n)` (#14817)

YaelDillies committed 2 years ago

cdb01be3

chore(topology/category/Top/limits): split file (#18871)

kim-em committed 2 years ago

178a3265

feat(data/set/pointwise/big_operators): image distributes across pointwise big operators (#18840)

eric-wieser committed 2 years ago

fa2cb8a9

Older