leanprover-community/mathlib

Pull Requests Commits

feat(analysis/special_functions/complex/arg): `arg_coe_angle_eq_iff` (#12017)

jsm28 committed 3 years ago

92ac8ff8

chore(number_theory/padics/padic_norm): golf `prod_pow_prime_padic_val_nat` (#12034)

stuart-presnell committed 3 years ago

5dc720d1

chore(category_theory/linear/yoneda): Removing some slow uses of `obviously` (#11979)

stuart-presnell committed 3 years ago

f9bac45c

refactor(topology/constructions): turn `cofinite_topology` into a type synonym (#11967)

urkud committed 3 years ago

efdce094

feat(algebra/covariant_and_contravariant): covariance and monotonicity (#11815)

ecstatic-morse committed 3 years ago

ec11e5f5

doc(number_theory/cyclotomic/gal): fix typo (#12038)

ericrbg committed 3 years ago

4ba83349

feat(data/nat/factorization): add `le_of_mem_factorization` (#12032)

stuart-presnell committed 3 years ago

263833cf

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

eric-wieser committed 3 years ago

1a3c0696

feat(data/list/big_operators): add `list.prod_map_mul` (#12029)

kmill committed 3 years ago

583ea58a

feat(algebra/star/self_adjoint): generalize scalar action instances (#12021)

eric-wieser committed 3 years ago

199e8ca8

feat(analysis/normed_space/linear_isometry): `trans_one`, `one_trans`, `refl_mul`, `mul_refl` (#12016)

jsm28 committed 3 years ago

5166aaab

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

stuart-presnell committed 3 years ago

d33792e6

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

BoltonBailey committed 3 years ago

132ea051

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

vihdzp committed 3 years ago

dce5dd4c

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

urkud committed 3 years ago

a87d431b

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

remove iff lemma

dupuisf committed 3 years ago

f76c10d9

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

Newer Older