leanprover-community/mathlib

Pull Requests Commits

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

feat(analysis/special_functions/integrals): integral of `|x - a| ^ n` over `Ι a b` (#9752)

urkud committed 4 years ago

3fe67d65

chore(topology/maps): add `is_closed_map.closed_range` (#9751)

urkud committed 4 years ago

54e9e120

chore(data/list/lex): make data.list.lex not depend on data.list.basic (#9750)

alexjbest committed 4 years ago

998ab788

feat(topology/G_delta): add lemmas, minor golf (#9742)

urkud committed 4 years ago

066a168d

feat(group_theory/subgroup/basic): Range of inclusion (#9732)

tb65536 committed 4 years ago

aa0d0d41

Newer Older