leanprover-community/mathlib

Pull Requests Commits

eric-wieser committed 3 years ago

89fe3411

eric-wieser committed 3 years ago

Verified 56de9440

Update set.lean

eric-wieser committed 3 years ago

Verified cf9d790b

chore(data/equiv/set): more lemmas about prod

eric-wieser committed 3 years ago

Verified db5f1861

feat(measure_theory/measure): more lemmas about `null_measurable_set`s (#12019)

urkud committed 3 years ago

2ceacc1a

chore(analysis): move some code (#12008)

urkud committed 3 years ago

25ebf419

feat(analysis/complex/isometry): `rotation_trans` (#12015)

jsm28 committed 3 years ago

26fd61c5

feat(order/filter/bases): basis of infimum of filters (#11855)

ADedecker committed 3 years ago

77dfac2e

feat(order/partition/finpartition): Finite partitions (#9795)

YaelDillies committed 3 years ago

6550cbac

feat(data/nat/factorization): add lemma `prod_prime_factors_dvd` (#11572)

stuart-presnell committed 3 years ago

f91a32d1

chore(number_theory/dioph): fix docs (#12011)

ericrbg committed 3 years ago

b08dc174

chore(measure_theory/integral/lebesgue): use to_additive when declaring instances and basic lemmas about simple functions (#12000)

RemyDegenne committed 3 years ago

af1355c4

chore(topology/algebra): rename file to match renamed lemmas (#11996)

eric-wieser committed 3 years ago

4b217ea7

chore(data/finset/basic): Golf and compress (#11987)

YaelDillies committed 3 years ago

4a4a3a90

chore(measure_theory/function/ae_eq_fun): replace topological assumptions by measurability assumptions (#11981)

RemyDegenne committed 3 years ago

5f70cd95

feat(group_theory/sylow): all max groups normal imply sylow normal (#11841)

nomeata committed 3 years ago

b72300f3

feat(analysis/analytic/basic): add uniqueness results for power series (#11896)

j-loreaux committed 3 years ago

06e7f767

feat(order/category/BoundedOrder): The category of bounded orders (#11961)

YaelDillies committed 3 years ago

91cc4ae6

chore(topology/algebra/ordered/*): Rename folder (#11988)

YaelDillies committed 3 years ago

1b5f8c28

chore(category_theory/monad/equiv_mon): Removing some slow uses of `obviously` (#11980)

stuart-presnell committed 3 years ago

7bebee66

chore(topology/algebra/module/multilinear): relax typeclass arguments (#11972)

eric-wieser committed 3 years ago

71e90063

refactor(measure_theory/group/basic): rename and split (#11952)

fpvandoorn committed 3 years ago

822244f7

feat(topology/instances/real): metric space structure on nat (#11963)

sgouezel committed 3 years ago

60d32337

feat(tactic/lint): add unprintable tactic linter (#11725)

digama0 committed 3 years ago

dff8393c

feat(category_theory/category/Twop): The category of two-pointed types (#11844)

YaelDillies committed 3 years ago

227293b5

chore(order/cover): Rename `covers` to `covby` (#11984)

YaelDillies committed 3 years ago

788240cf

doc(data/finset/basic): correct some function names (#11983)

kmill committed 3 years ago

3fcb7380

refactor(data/nat/factorization): Use factorization instead of factors.count (#11384)

b-mehta committed 3 years ago

515ce797

feat(measure_theory/measure/haar_quotient): Pushforward of Haar measure is Haar (#11593)

AlexKontorovich committed 3 years ago

da76d218

feat(number_theory/number_field/basic) : the ring of integers of a number field is not a field (#11956)

mariainesdff committed 3 years ago

edefc116

Older