leanprover-community/mathlib

Pull Requests Commits

Tidy divisibility; start `prime_factorization_inverse_prod_pow`

stuart-presnell committed 4 years ago

9d2118a8

Update to note PR #10536

stuart-presnell committed 4 years ago

17aeaf79

stuart-presnell committed 4 years ago

ee37af87

Update factorization_via_finsupp.lean

stuart-presnell committed 4 years ago

d50aacca

Added `prime_pow_of_prime_factorization_single`

stuart-presnell committed 4 years ago

3941bda8

Improve lemma: `factor_iff_mem_factorization`

stuart-presnell committed 4 years ago

7b81edbb

Create factorization_via_finsupp.lean

stuart-presnell committed 4 years ago

ce4a432a

refactor(topology,algebraic_geometry): use bundled maps here and there (#10447)

urkud committed 4 years ago

d487d650

feat(topology/uniform_space/uniform_convergence): slightly generalize theorems (#10444)

urkud committed 4 years ago

3590dc29

feat(topology/sheaves): Generalized some lemmas. (#10440)

erdOne committed 4 years ago

8d07dbf4

chore(ring_theory/polynomial/cyclotomic): use `ratfunc` (#10421)

Vierkantor committed 4 years ago

a086daa5

feat(category_theory/limits): Results about (co)limits in Top (#9985)

erdOne committed 4 years ago

6cb52e67

chore(topology): add 2 missing `inhabited` instances (#10446)

urkud committed 4 years ago

d267b6ca

chore(scripts): update nolints.txt (#10445)

leanprover-community-bot committed 4 years ago

1c001794

feat(measure_theory): TC for smul-invariant measures (#10325)

urkud committed 4 years ago

f578d1d6

feat(ring_theory/adjoin/basic): add adjoin_induction' and adjoin_adjoin_coe_preimage (#10427)

riccardobrasca committed 4 years ago

0cbba1a4

feat(analysis): derivative of a parametric interval integral (#10404)

urkud committed 4 years ago

c192937f

feat(data/nat/prime): some lemmas about prime factors (#10385)

stuart-presnell committed 4 years ago

ac283c22

feat(linear_algebra/affine_space/barycentric_coords): characterise affine bases in terms of coordinate matrices (#10370)

ocfnash committed 4 years ago

eb8b1b82

feat(data/mv_polynomial/basic): add a symmetric version of coeff_X_mul and generalize to monomials (#10429)

eric-wieser committed 4 years ago

fb82d0a5

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

Older