leanprover-community/mathlib

Pull Requests Commits

golf downstream results

eric-wieser committed 2 years ago

505842d2

Merge remote-tracking branch 'origin/master' into eric-wieser/bounded_smul

eric-wieser committed 2 years ago

77d2fc01

more elaboration help

eric-wieser committed 2 years ago

88c9b450

unification help

eric-wieser committed 2 years ago

fadeec4a

unification help

eric-wieser committed 2 years ago

0e72a203

feat(measure_theory/function/l1_space): generalize from fields to rings (#19052)

eric-wieser committed 2 years ago

9b33e5f3

eric-wieser committed 2 years ago

1810133f

eric-wieser committed 2 years ago

f45f9259

refactor(analysis/normed_space/basic): generalize some results to actions by normed_rings

eric-wieser committed 2 years ago

c4afcafd

feat(combinatorics/simple_graph/regularity): Increment partition (#19051)

YaelDillies committed 2 years ago

bf7ef0e8

feat(combinatorics/simple_graph/regularity/chunk): Partition of a part (#18371)

YaelDillies committed 2 years ago

f51de876

chore(.github/workflows): don't rely on linkifier in maintainer merge messages (#19046)

kim-em committed 2 years ago

ef7403fe

chore(ring_theory/localization/away): split (#19041)

kim-em committed 2 years ago

a7c017d7

chore(analysis/convex/cone/basic): split (#19043)

hrmacbeth committed 2 years ago

915591b2

feat(linear_algebra/matrix/charpoly/minpoly): `minpoly` is unaffected by `to_lin` and `to_matrix` (#19036)

eric-wieser committed 2 years ago

7ae139f9

chore(measure_theory/{constructions/prod,measure/lebesgue}): split (#19039)

hrmacbeth committed 2 years ago

fd5edc43

feat(topology/algebra/module/star): continuity results for star_modules (#19037)

eric-wieser committed 2 years ago

aa666983

chore(measure_theory/special_functions/basic): split (#19040)

hrmacbeth committed 2 years ago

83a66c87

chore(category_theory/monoidal/types): split file (#19035)

kim-em committed 2 years ago

95a87616

chore(algebra/category/Module/monoidal): split file (#19034)

kim-em committed 2 years ago

74403a3b

chore(data/set/Union_lift) generalize Union_lift to Sort (#19033)

ChrisHughes24 committed 2 years ago

5a4ea845

refactor(analysis/convex/specific_functions): split (#19031)

hrmacbeth committed 2 years ago

8f9fea08

feat(field_theory/minpoly/basic): `minpoly` is unaffected by injective `alg_hom`s (#19030)

eric-wieser committed 2 years ago

df0098f0

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

leanprover-community-bot committed 2 years ago

50251fd6

chore(number_theory/modular_forms): don't define jacobi_theta on subtype (#19029)

loefflerd committed 2 years ago

c720ca16

feat(algebra/category/Module/change_of_rings): coextension of scalars (#15958)

jjaassoonn committed 2 years ago

56b71f0b

feat(nat/factorial): add double factorials (#18994)

jakelev committed 2 years ago

7daeaf30

feat(analysis/convex/specific_functions): elementary convexity proofs (#19026)

hrmacbeth committed 2 years ago

a8b2226c

feat(geometry/manifold/vector_bundle/hom): the hom bundle is smooth (#18828)

fpvandoorn committed 2 years ago

c89fe2d5

feat(geometry/manifold/cont_mdiff_mfderiv): prove that mfderiv is smooth (#18827)

fpvandoorn committed 2 years ago

17fe3632

Older