leanprover-community/mathlib3

Pull Requests Commits

EPronovost committed 4 years ago

012f85ac

feat(list/prod_monoid): add list.prod_map* lemmas

EPronovost committed 4 years ago

84751880

chore(data/finset/basic): finset.prod -> finset.product in module docstring (#10413)

kmill committed 4 years ago

9277d4b4

chore(*): golf proofs about `filter.Coprod` (#10400)

urkud committed 4 years ago

d17db717

feat(linear_algebra/bilinear_map): semilinearize bilinear maps (#10373)

dupuisf committed 4 years ago

d98b8e0e

feat(measure_theory/covering/differentiation): differentiation of measures (#10101)

sgouezel committed 4 years ago

8f07d75b

feat(measure_theory): define volume on `complex` (#10403)

urkud committed 4 years ago

8ee634b0

feat(analysis/inner_product_space/projection): orthogonal group is generated by reflections (#10381)

hrmacbeth committed 4 years ago

2168297e

feat(topology/separation): removing a finite set from a dense set preserves density (#10405)

sgouezel committed 4 years ago

e0c0d84a

feat(measure_theory): measure preserving maps and integrals (#10326)

urkud committed 4 years ago

55b81f8b

feat(data/finset/basic): add filter_erase (#10384)

BoltonBailey committed 4 years ago

2a286527

feat(data/nat/interval): add Ico_succ_left_eq_erase (#10386)

BoltonBailey committed 4 years ago

32c05079

feat(topology/algebra/infinite_sum): add `has_sum.smul_const` etc (#10393)

urkud committed 4 years ago

b3538bfa

feat(analysis/special_functions/complex/arg): review, golf, lemmas (#10365)

urkud committed 4 years ago

618447fa

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

leanprover-community-bot committed 4 years ago

bd6c6d54

chore(category_theory/limits/shapes/pullbacks): fix diagrams in docs (#10379)

Ruben-VandeVelde committed 4 years ago

db926f00

doc(topology/separation): two typos (#10382)

fpvandoorn committed 4 years ago

7638fe21

refactor(algebra/opposites): use mul_opposite for multiplicative opposite (#10302)

eric-wieser committed 4 years ago

e8858fdd

feat(*): Reduce imports to only those necessary in the entire library (#10349)

alexjbest committed 4 years ago

d6814c58

feat(data/polynomial/eval): is_root_(prod/map) (#10360)

ericrbg committed 4 years ago

5000fb02

feat(analysis/calculus/deriv): generalize lemmas about deriv and `smul` (#10378)

urkud committed 4 years ago

784fe06d

feat(logic/basic): define exists_unique_eq as a simp lemma (#10364)

Julian committed 4 years ago

f3f44425

feat(field_theory/splitting_field): add a more general algebra instance as a def (#10220)

eric-wieser committed 4 years ago

d5d2c4f6

feat(topology/algebra/module): add `is_scalar_tower` and `smul_comm_class` instances for `continuous_linear_map` (#10375)

urkud committed 4 years ago

96540719

feat(measure_theory/integral/{set_to_l1,bochner}): generalize results about integrals to `set_to_fun` (#10369)

RemyDegenne committed 4 years ago

0d09e993

chore(analysis/calculus): use `is_R_or_C` in several lemmas (#10376)

urkud committed 4 years ago

0ededd5d

doc(order/monotone): fix 2 typos (#10377)

urkud committed 4 years ago

198ed6bb

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

leanprover-community-bot committed 4 years ago

2f3b1852

chore(.docker): don't install unnecessary toolchains (#10363)

kim-em committed 4 years ago

f8cbb3e4

feat(data/nat/parity): add lemmas (#10352)

riccardobrasca committed 4 years ago

5d1363ea

Older