leanprover-community/mathlib3

Pull Requests Commits

feat(analysis/normed_space/add_torsor_bases): the convex hull has non-empty interior iff the affine span is top (#9727)

ocfnash committed 4 years ago

39db98c8

chore(field_theory/galois): speedup a slow convert (#9782)

kim-em committed 4 years ago

2e62b33c

feat(linear_algebra/affine_space/independent): affine equivalences preserve affine independence of sets of points (#9776)

ocfnash committed 4 years ago

27d28a84

feat(topology/metric_space): closed if spaced out (#9754)

urkud committed 4 years ago

fb5c0bec

split(data/list/permutation): split off `data.list.basic` (#9749)

YaelDillies committed 4 years ago

6cd6ff44

refactor(linear_algebra/quadratic_form): split file (#9781)

kim-em committed 4 years ago

5b527bd0

feat(data/nat/gcd): `coprime.lcm_eq_mul` (#9761)

tb65536 committed 4 years ago

27a777b1

feat(topology/metric_space): a map with a contracting iterate has a fixed pt (#9760)

urkud committed 4 years ago

5dbe8c48

chore(analysis/normed_algebra/exponential): golf, generalize (#9740)

urkud committed 4 years ago

084702d0

chore(data/finset/lattice): fix infi docstrings (#9775)

pechersky committed 4 years ago

376bba8a

chore(topology/algebra/ordered/basic): move code out of `basic` (#9772)

urkud committed 4 years ago

41b56455

feat(topology/algebra/mul_action): `λ x, c • x` is a closed map for all `c` (#9756)

urkud committed 4 years ago

1432c308

feat(measure_theory/measure): +1 version of Borel-Cantelli, drop an assumption (#9678)

urkud committed 4 years ago

48dc2492

chore(analysis/p_series): use `lift` tactic (#9773)

urkud committed 4 years ago

3f15148f

feat(group_theory/index): `index_comap_of_surjective` (#9768)

tb65536 committed 4 years ago

9fec8f35

feat(topology/instances/ennreal): `{f | lipschitz_with K f}` is a closed set (#9766)

urkud committed 4 years ago

85f36400

chore(data/equiv/mul_add): add missing `to_equiv_mk` (#9765)

urkud committed 4 years ago

678d7edf

feat(data/nat/gcd): Add `iff` version of `coprime.dvd_of_dvd_mul` (#9759)

tb65536 committed 4 years ago

24ebeece

feat(group_theory/subgroup/basic): Special cases of `subgroup_of` (#9755)

tb65536 committed 4 years ago

1558a767

refactor(ring_theory/jacobson): avoid shadowing hypothesis (#9736)

kim-em committed 4 years ago

4b00aa2d

feat(topology/homotopy): Define the fundamental groupoid of a topological space (#9683)

shingtaklam1324 committed 4 years ago

5eb47c00

feat(linear_algebra/affine_space/independent): add `exists_affine_independent` (#9747)

ocfnash committed 4 years ago

f171c615

feat(group_theory/subgroup/basic): Kernel of `subtype` and `inclusion` (#9763)

tb65536 committed 4 years ago

ff8a35d4

chore(group_theory/quotient_group): Tag lemmas with `@[to_additive]` (#9771)

tb65536 committed 4 years ago

7aa431c9

chore(measure_theory/*): don't require the codomain to be a normed group (#9769)

urkud committed 4 years ago

a1a05ad8

chore(topology/instances/ennreal): golf a proof (#9767)

urkud committed 4 years ago

08a070b4

chore(analysis/normed/group): add a few convenience lemmas (#9770)

urkud committed 4 years ago

4a837fb9

refactor(group_theory/quotient_group): Fix typo (#9746)

tb65536 committed 4 years ago

cf72eff0

feat(set_theory/cardinal): cardinal.to_nat_congr (#9726)

tb65536 committed 4 years ago

ad7000b9

feat(set_theory/cardinal): lemmas (#9690)

kim-em committed 4 years ago

b97bb92f

Newer Older