leanprover-community/mathlib

Pull Requests Commits

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

riccardobrasca committed 4 years ago

5d1363ea

feat(linear_algebra/bilinear_form): add lemmas (#10353)

riccardobrasca committed 4 years ago

276ab17f

urkud committed 4 years ago

4d1f92ad

Merge branch 'master' of git://github.com/leanprover-community/mathlib into YK-smul-inv-meas

urkud committed 4 years ago

066003e4

chore(measure_theory/group/basic): drop measurability assumption (#10367)

urkud committed 4 years ago

6f793bb0

chore(category_theory/filtered): slightly golf two proofs (#10368)

Ruben-VandeVelde committed 4 years ago

e14e87ae

urkud committed 4 years ago

7b6160ca

Merge branch 'YK-smul-inv-meas' into YK-integral-fundamental

urkud committed 4 years ago

98671682

Merge branch 'YK-inv-apply' into YK-smul-inv-meas

urkud committed 4 years ago

0ec18b78

chore(measure_theory/group/basic): drop measurability assumption

urkud committed 4 years ago

83965a02

Merge remote-tracking branch 'origin/master' into YK-smul-inv-meas

urkud committed 4 years ago

1f96a894

Merge branch 'master' into YK-smul-inv-meas

urkud committed 4 years ago

ab3344f5

feat(linear_algebra/bilinear_form): add lemmas about congr (#10362)

eric-wieser committed 4 years ago

c7441af1

chore(analysis/inner_product_space/projection): typeclass inference for completeness (#10357)

hrmacbeth committed 4 years ago

568435cb

chore(analysis/mean_inequalities): split mean_inequalities into two files (#10355)

RemyDegenne committed 4 years ago

d5c2b34c

feat(finset/basic): Adding `list.to_finset_union` and `list.to_finset_inter` (#10351)

stuart-presnell committed 4 years ago

60363a4e

lint(*): curly braces linter (#10280)

jcommelin committed 4 years ago

8f6fd1b6

feat(order/imp): define `lattice.imp` and `lattice.biimp` (#10327)

urkud committed 4 years ago

2bdadb4f

feat(combinatorics/set_family/shadow): Shadow of a set family (#10223)

YaelDillies committed 4 years ago

0a2a9229

feat(topology/metric_space/hausdorff_distance): add definition and lemmas about open thickenings of subsets (#10188)

kkytola committed 4 years ago

7fec4014

feat(number_theory/divisors): mem_divisors_self (#10359)

ericrbg committed 4 years ago

bce0ede7

refactor(linear_algebra/bilinear_form): Change namespace of is_refl, is_symm, and is_alt (#10338)

mcdoll committed 4 years ago

8f7971ae

feat(data/fin/basic): add lemmas about fin.cast (#10329)

eric-wieser committed 4 years ago

698eb1e3

feat(topology/uniform_space): properties of uniform convergence (#9958)

fpvandoorn committed 4 years ago

9fa14a60

feat(number_theory): define the class number (#9071)

Vierkantor committed 4 years ago

d6b83d87

feat(dynamics): define `{mul,add}_action.is_minimal` (#10311)

urkud committed 4 years ago

f7807881

feat(linear_algebra/sesquilinear_form): Add is_refl for sesq_form.is_alt (#10341)

mcdoll committed 4 years ago

d36f17f8

feat(linear_algebra/determinant): the determinant associated to the standard basis of the free module is the usual matrix determinant (#10278)

ocfnash committed 4 years ago

7f4b91b0

feat(field_theory): define the field of rational functions `ratfunc` (#9563)

Vierkantor committed 4 years ago

e20af159

chore(order/filter/basic): add 2 trivial `simp` lemmas (#10344)

urkud committed 4 years ago

f01399c4

Newer Older