leanprover-community/mathlib3

Pull Requests Commits

feat (order/lexicographic): add API lemmas (#10887)

MantasBaksys committed 4 years ago

faee3582

chore(order/complete_lattice): eliminate `finish` (#10876)

stuart-presnell committed 4 years ago

45ed9ded

feat(data/list/count): add lemma `list.count_singleton'` (#10880)

stuart-presnell committed 4 years ago

68d9b42b

some_lemmas.lean is gone

jjaassoonn committed 4 years ago

157cd238

moved another lemma in some_lemmas to correct location with correct name

jjaassoonn committed 4 years ago

f1f3470c

jjaassoonn committed 4 years ago

de3765d7

feat(algebra/group_power/basic): generalize `zpow_neg_one` to `div_inv_monoid` (#10894)

urkud committed 4 years ago

9e5cbc12

feat(analysis/asymptotics): add `is_O.inv_rev`, `is_o.inv_rev` (#10896)

urkud committed 4 years ago

3fc32e3e

chore(algebra/iterate_hom): use to_additive to fill missing lemmas (#10886)

eric-wieser committed 4 years ago

72224634

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

leanprover-community-bot committed 4 years ago

a2c3b293

refactor(measure_theory/measure/hausdorff): change Hausdorff measure definition at 0 (#10859)

sgouezel committed 4 years ago

ee17ab3a

chore(category_theory/monoidal/End): Adding API for monoidal functors into `C ⥤ C` (#10841)

erdOne committed 4 years ago

289ebe58

feat(linear_algebra/determinant): more properties of the determinant of linear maps (#10809)

sgouezel committed 4 years ago

9f1b9bcd

feat(topology/metric/hausdorff_distance): more properties of cthickening (#10808)

sgouezel committed 4 years ago

0d473696

feat(linear_algebra/affine_space/affine_equiv): isomorphism with the units (#10798)

eric-wieser committed 4 years ago

a6179f61

split(data/finset/*): Split `data.finset.card` and `data.finset.fin` off `data.finset.basic` (#10796)

YaelDillies committed 4 years ago

2c4e66f7

feat(linear_algebra/affine_space/combination): vsub distributivity lemmas (#10786)

jsm28 committed 4 years ago

fa46ef10

feat(algebraic_geometry/open_immersion): Easy results about open immersions. (#10776)

erdOne committed 4 years ago

ecec43a2

feat(field_theory/splitting_field): generalize some results from field to domain (#10726)

alexjbest committed 4 years ago

6e59fbe3

feat(order/cover): The covering relation (#10676)

YaelDillies committed 4 years ago

fec084c3

I forget to commit the change

jjaassoonn committed 4 years ago

d38b3b02

jjaassoonn committed 4 years ago

7a8971c8

jjaassoonn committed 4 years ago

3e3188c9

one less lemma in some_lemmas.lean

jjaassoonn committed 4 years ago

3c4dcd1a

feat(algebra/group/inj_surj): _pow definitions for surjective too (#10832)

eric-wieser committed 4 years ago

011203d9

feat(data/matrix/rank): rank of a matrix (#10826)

jcommelin committed 4 years ago

59152548

feat(linear_algebra/orientation): add orientation.map (#10815)

eric-wieser committed 4 years ago

915e2b5b

feat(ring_theory/prinicipal_ideal_domain): Bézout's lemma for PIDs (#10810)

Ruben-VandeVelde committed 4 years ago

e70faf34

feat(linear_algebra/affine_space/affine_subspace): affine_subspace.comap (#10795)

eric-wieser committed 4 years ago

47c676ed

feat(topology/algebra/mul_action): add an instance in the presence of `is_central_scalar` (#10787)

eric-wieser committed 4 years ago

00454f23

Newer Older