leanprover-community/mathlib

Pull Requests Commits

chore(linear_algebra/finite_dimensional): add some irreducible

kim-em committed 2 years ago

961da82a

chore(.github/workflows): update gh-get-current-pr (#18763)

alexjbest committed 2 years ago

d20a8cd5

feat (measure_theory/integral): lemmas `integral_Ioi_eq_integral_Ici` etc (#18899)

loefflerd committed 2 years ago

8b8ba04e

chore(linear_algebra/matrix/to_linear_equiv): golf using existing morphisms (#18895)

eric-wieser committed 2 years ago

e42cfdb0

feat(analysis/fourier): Riemann-Lebesgue lemma (#17719)

loefflerd committed 2 years ago

9425b6f8

chore(data/finset/lattice): Move lemmas around (#18900)

YaelDillies committed 2 years ago

9d684a89

feat(ring_theory/ideal/quotient_operations): add double quotient of an algebra (#18452)

wupr committed 2 years ago

b88d81c8

feat(data/set/intervals/basic): generalize from `linear_order` to `preorder` (#18876)

eric-wieser committed 2 years ago

4367b192

feat(data/set/intervals/pi): `f.update i '' Icc a b = Icc (f.update i a) (f.update i b)` (#18892)

YaelDillies committed 2 years ago

e4bc74cb

chore (measure_theory/integral): split interval_integral.lean into two (#18898)

loefflerd committed 2 years ago

011cafb4

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

Older