leanprover-community/mathlib3

Pull Requests Commits

feat(data/nat/factorization): add lemma `factorization_gcd` (#11605)

stuart-presnell committed 4 years ago

d33792e6

docs(computability/partrec_code): add docs (#11929)

BoltonBailey committed 4 years ago

132ea051

feat(order/well_founded, set_theory/ordinal_arithmetic): `eq_strict_mono_iff_eq_range` (#11882)

vihdzp committed 4 years ago

dce5dd4c

feat(topology/algebra): add `@[to_additive]` to some lemmas (#12018)

urkud committed 4 years ago

a87d431b

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

urkud committed 4 years ago

2ceacc1a

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

urkud committed 4 years ago

25ebf419

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

jsm28 committed 4 years ago

26fd61c5

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

ADedecker committed 4 years ago

77dfac2e

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

YaelDillies committed 4 years ago

6550cbac

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

stuart-presnell committed 4 years ago

f91a32d1

awainverse committed 4 years ago

8ae9e62f

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

ericrbg committed 4 years ago

b08dc174

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

RemyDegenne committed 4 years ago

af1355c4

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

eric-wieser committed 4 years ago

4b217ea7

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

YaelDillies committed 4 years ago

4a4a3a90

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

RemyDegenne committed 4 years ago

5f70cd95

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

nomeata committed 4 years ago

b72300f3

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

j-loreaux committed 4 years ago

06e7f767

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

YaelDillies committed 4 years ago

91cc4ae6

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

YaelDillies committed 4 years ago

1b5f8c28

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

stuart-presnell committed 4 years ago

7bebee66

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

eric-wieser committed 4 years ago

71e90063

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

fpvandoorn committed 4 years ago

822244f7

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

sgouezel committed 4 years ago

60d32337

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

digama0 committed 4 years ago

dff8393c

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

YaelDillies committed 4 years ago

227293b5

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

YaelDillies committed 4 years ago

788240cf

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

kmill committed 4 years ago

3fcb7380

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

b-mehta committed 4 years ago

515ce797

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

AlexKontorovich committed 4 years ago

da76d218

Newer Older