leanprover-community/mathlib

Pull Requests Commits

ADedecker committed 4 years ago

2da2c8c7

ADedecker committed 4 years ago

9ea582d2

ADedecker committed 4 years ago

fc3de86f

ADedecker committed 4 years ago

779e8253

ADedecker committed 4 years ago

de8b8c74

Merge branch 'set_integral_congr_set_ae' into integral_test

ADedecker committed 4 years ago

880ae586

set integral is compatible with ae-eq of sets

ADedecker committed 4 years ago

59f989eb

feat(group_theory/subgroup): eq_top_of_le_card and eq_bot_of_card_le (#8414)

tb65536 committed 4 years ago

0190177e

chore(data/pnat/basic): rename `bot_eq_zero` to `bot_eq_one`, generalize from `Prop` to `Sort*` (#8412)

YaelDillies committed 4 years ago

d8fc0817

feat(ring_theory): shortcut lemmas for `coe : ideal R → fractional_ideal R⁰ K` (#8395)

Vierkantor committed 4 years ago

1dc4bef9

feat(ring_theory): (fractional) ideals are finitely generated if they are invertible (#8294)

Vierkantor committed 4 years ago

708b25d2

feat(data/fintype/basic): provide a `fintype` instance for `sym α n` (#8427)

YaelDillies committed 4 years ago

4ca0a8b3

feat(data/fintype/basic): add `finset.(sup|inf)_univ_eq_(supr|infi)` (#8397)

eric-wieser committed 4 years ago

740b41bd

chore(*): standardize Prop/Type instance names (#8360)

ericrbg committed 4 years ago

0c024a62

feat(linear_algebra/matrix/determinant): det_pow (#8421)

pechersky committed 4 years ago

24403303

feat(measure_theory/vector_measure): add partial order instance to vector measures (#8410)

kex-y committed 4 years ago

fff96e53

feat(group_theory/subgroup): eq_bot_of_card_eq (#8413)

tb65536 committed 4 years ago

02b37b5a

feat(group_theory/complement): define subgroup complement, prove Schur-Zassenhaus (#8008)

tb65536 committed 4 years ago

8a0d5e07

refactor(data/set/disjointed): split into `data.set.pairwise` and `order.disjointed` (#8411)

YaelDillies committed 4 years ago

3d11f2da

feat(analysis/normed_space/linear_isometry): add an upgrade from linear isometries between finite dimensional spaces of eq finrank to linear isometry equivs (#8406)

justadzr committed 4 years ago

dfa95abf

feat(topology/locally_constant): Adding a module structure to locally constant functions (#8384)

laughinggas committed 4 years ago

8062521e

feat(set/basic): range_splitting f : range f → α (#8340)

kim-em committed 4 years ago

f2f62286

fix(data/polynomial): Resolve a has_scalar instance diamond (#8392)

eric-wieser committed 4 years ago

6efc3e91

feat(analysis/calculus): strictly differentiable (or C^1) map is locally Lipschitz (#8362)

urkud committed 4 years ago

ced1f120

feat(measure_theory/integrable_on): a monotone function is integrable on any compact subset (#8336)

ADedecker committed 4 years ago

1dafd0f7

refactor(topology/metric_space): move lemmas about `paracompact_space` and the shrinking lemma to separate files (#8404)

urkud committed 4 years ago

970b17bf

chore(topology/urysohns_lemma): use bundled `C(X, ℝ)` (#8402)

urkud committed 4 years ago

0dd81c1e

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

leanprover-community-bot committed 4 years ago

88de9b51

feat(measure_theory/measure_space): add measurable set lemma for symmetric differences (#8401)

kex-y committed 4 years ago

316d69fe

feat(linear_algebra/matrix/determinant): generalize det_fin_zero to det_eq_one_of_is_empty (#8387)

eric-wieser committed 4 years ago

0cbc6f39

Older