leanprover-community/mathlib3

Pull Requests Commits

feat(data/nat/prime): stronger sublist factor lemmas

b-mehta committed 4 years ago

Verified 6ce29940

feat(group_theory/coset): Embeddings of quotients (#10901)

tb65536 committed 4 years ago

b02e2ea1

feat(analysis/calculus/{f,}deriv): generalize `has_fderiv_at_filter.is_O_sub_rev` (#10897)

urkud committed 4 years ago

b4961da2

feat(combinatorics/simple_graph/matching): is_matching iff all degrees = 1 (#10864)

arthurpaulino committed 4 years ago

bcf20b09

feat(ring_theory/polynomial/cyclotomic): generalize a few results to domains (#10741)

alexjbest committed 4 years ago

19290257

feat(group_theory/index): `relindex_eq_zero_of_le_left` (#10902)

tb65536 committed 4 years ago

5a790471

feat(ring_theory/integral_closure): `is_field_iff_is_field` (#10875)

tb65536 committed 4 years ago

5c05ca28

feat(data/polynomial): add some simp attributes and commuted versions of coeff_mul_X_pow (#10868)

alexjbest committed 4 years ago

d5de8eac

feat(algebraic_geometry): Open immersions of locally ringed spaces have pullbacks (#10917)

erdOne committed 4 years ago

ade581e9

feat(order/monotone): Functions from/to subsingletons are monotone (#10903)

YaelDillies committed 4 years ago

093aef54

refactor(data/polynomial/eval): Golf `hom_eval₂` (#10920)

tb65536 committed 4 years ago

1067556a

feat(docs/references) : Added reference for #10791 (#10915)

erdOne committed 4 years ago

c40c7013

feat(data/finset/basic): add image_congr (#10911)

AntoineChambert-Loir committed 4 years ago

9cbd828a

refactor(ring_theory/tensor_product): Speed up slow proofs (#10883)

tb65536 committed 4 years ago

f7b24fa7

chore(category_theory/filtered): avoid `finish` (#10918)

Ruben-VandeVelde committed 4 years ago

6ab0f909

feat(algebra/algebra/subalgebra): `subalgebra.map` commutes with supremum (#10899)

tb65536 committed 4 years ago

5dd35377

feat(ring_theory/tensor_product): The tensor product `A ⊗ B` is generated by tensors `a ⊗ₜ b` (#10900)

tb65536 committed 4 years ago

41ced1ca

feat(order/monotone): add `monotone_int_of_le_succ` etc (#10895)

urkud committed 4 years ago

194bde8f

feat(data/list/sort): subperm sorted implies sublist (#10892)

b-mehta committed 4 years ago

a60ef7c9

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

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

Older