leanprover-community/mathlib

Pull Requests Commits

feat(category_theory/sites/*): Comparison lemma (#9785)

erdOne committed 4 years ago

ba43124c

feat(topology/algebra/ordered): convergent sequence is bounded above/below (#10424)

urkud committed 4 years ago

a779f6cf

feat(algebra/big_operators/order): Bounding on a sum of cards by double counting (#10389)

YaelDillies committed 4 years ago

1dd3ae1c

chore(algebra/algebra and group_theory/group_action): move a lemma (#10425)

j-loreaux committed 4 years ago

b14f22e9

feat(measure_theory): add `is_R_or_C.measurable_space` (#10417)

urkud committed 4 years ago

7c4f395a

feat(linear_algebra/affine_space/barycentric_coords): affine bases exist over fields (#10333)

ocfnash committed 4 years ago

a1338d62

feat(group_theory/schur_zassenhaus): Prove the full Schur-Zassenhaus theorem (#10283)

tb65536 committed 4 years ago

7a6e6d8b

feat(combinatorics): Hindman's theorem on finite sums (#10029)

dwarn committed 4 years ago

97186fe6

doc(measure_theory/decomposition/jordan): typo (#10430)

fpvandoorn committed 4 years ago

050482cb

feat(field_theory): generalize `ratfunc K` to `comm_ring K`/`is_domain K` (#10428)

Vierkantor committed 4 years ago

53bd9d73

doc(field_theory/abel_ruffini): update module doc (#10426)

fpvandoorn committed 4 years ago

79582514

refactor(algebra.group.basic): Convert sub_add_cancel and neg_sub to multaplicative form (#10419)

mans0954 committed 4 years ago

2b754933

feat(logic/function/basic): add `function.{in,sur,bi}jective.comp_left` (#10406)

eric-wieser committed 4 years ago

d0e454ac

chore(measure_theory/integral): generalize `interval_integral.norm_integral_le_integral_norm` (#10412)

urkud committed 4 years ago

d9e40b44

chore(measure_theory/integral): add `integrable_const` for `interval_integral` (#10410)

urkud committed 4 years ago

28177886

chore(measure_theory/integral): more versions of `integral_finset_sum` (#10394)

urkud committed 4 years ago

3b137447

feat(topology/connected): sufficient conditions for the preimage of a connected set to be connected (#10289)

YaelDillies committed 4 years ago

2ec6de7d

feat(group_theory/exponent): Define the exponent of a group (#10249)

Julian-Kuelshammer committed 4 years ago

e8386bd4

refactor(*): split `order_{top,bot}` from `lattice` hierarchy (#9891)

pechersky committed 4 years ago

cf917732

chore(control/random): Move from `system.random.basic` (#10408)

YaelDillies committed 4 years ago

3fee4b9b

feat(analysis/normed_space/multilinear): add `norm_mk_pi_field` (#10396)

urkud committed 4 years ago

b1a9c2e4

chore(field_theory/separable): generalize theorems (#10337)

ericrbg committed 4 years ago

87b0084b

feat(order/filter/pi): define `filter.pi` and prove some properties (#10323)

urkud committed 4 years ago

9cf6766f

feat(linear_algebra/affine_space/barycentric_coords): barycentric coordinates are ratio of determinants (#10320)

ocfnash committed 4 years ago

33ea4012

feat(algebra/big_operators/finprod): add finprod_div_distrib and finsum_sub_distrib (#10044)

alexjbest committed 4 years ago

d94772bb

chore(measure_theory/integral): generalize `integral_smul_const` (#10411)

urkud committed 4 years ago

ac712929

chore(data/complex): add a few simp lemmas (#10395)

urkud committed 4 years ago

8f681f12

feat(data/complex/exponential): Add lemma add_one_le_exp (#10358)

isadofschi committed 4 years ago

4d5d7708

feat(algebraic_geometry, category_theory): SheafedSpace has colimits (#10401)

erdOne committed 4 years ago

6050f9df

refactor(ring_theory/sub[semi]ring): move pointwise instances to their own file (#10347)

eric-wieser committed 4 years ago

ca7347c4

Newer Older