leanprover-community/mathlib3

Pull Requests Commits

feat(topology/uniform_space): lemmas about `s ○ s ○ ... ○ s ⊆ t` (#14051)

urkud committed 3 years ago

6a48b384

feat(data/list/{count,perm},data/multiset/basic): countp and count lemmas (#14108)

kmill committed 3 years ago

3185c251

chore(data/real/ennreal): tidy some proofs (#14101)

Ruben-VandeVelde committed 3 years ago

23a22058

feat(set_theory/ordinal/basic): Order isomorphism between `o.out.α` and `set.Iio o` (#14074)

vihdzp committed 3 years ago

7b7af48b

feat(topology/uniform_space/separation): add `filter.has_basis.mem_separation_rel` (#14050)

urkud committed 3 years ago

26f41120

feat(number_theory/von_mangoldt): simple bounds on von mangoldt function (#14033)

b-mehta committed 3 years ago

a2e671bb

feat(set_theory/cardinal/cofinality): Move fundamental sequence results to namespace (#14020)

vihdzp committed 3 years ago

644cae5e

feat(order/filter/lift): drop an unneeded assumption (#14117)

urkud committed 3 years ago

c53285a8

chore(algebra/order/field): fill in TODO for inv anti lemmas (#14112)

b-mehta committed 3 years ago

85124aff

chore(algebra/order/field): fill in missing lemma (#14111)

b-mehta committed 3 years ago

462b9509

feat(data/polynomial/degree/lemmas): two lemmas about `nat_degree`s of sums (#14100)

adomani committed 3 years ago

f6178629

feat(topology/basic): add lemmas like `closure s \ interior s = frontier s` (#14086)

urkud committed 3 years ago

de418aad

feat(data/set/prod): add `prod_self_{s,}subset_prod_self` (#14084)

urkud committed 3 years ago

15f6b527

feat(topology/basic): add `nhds_basis_closeds` (#14083)

urkud committed 3 years ago

14749964

feat(topology/order): add `nhds_true` and `nhds_false` (#14082)

urkud committed 3 years ago

bb97a64b

perf(field_theory/primitive_element): declare auxiliary function `noncomputable!` (#14071)

Vierkantor committed 3 years ago

bd5914f6

feat(data/real/nnreal): add `nnreal.le_infi_add_infi` and other lemmas (#14048)

urkud committed 3 years ago

c4c279e6

feat(linear_algebra/tensor_product): tensor_product.map is bilinear in its two arguments (#13608)

antoinelab01 committed 3 years ago

a945b187

feat(algebra/big_operators/basic): add `sum_erase_lt_of_pos` (#14066)

stuart-presnell committed 3 years ago

17102ae8

feat(data/nat/factorization): three lemmas on the components of factorizations (#14031)

stuart-presnell committed 3 years ago

86d58ae7

feat(data/nat/basic): four lemmas on nat and int division (#13991)

stuart-presnell committed 3 years ago

3c1ced3b

feat(data/sym/sym2): simp lemma for quotient.eq (#14113)

kmill committed 3 years ago

4b3988ad

doc(data/matrix/basic): Clarify docstring (#14109)

kbuzzard committed 3 years ago

3d030983

feat(number_theory/divisors): add `filter_dvd_eq_proper_divisors` (#14049)

stuart-presnell committed 3 years ago

27e7f7ac

doc(tactic/rewrite_search/explain): Fix documentation-breaking docstring (#14107)

eric-wieser committed 3 years ago

3b185739

chore(data/nat/multiplicity): simplify proof (#14103)

ChrisHughes24 committed 3 years ago

0e834dfe

fix(analysis/special_functions/pow): fix norm_num extension (#14099)

digama0 committed 3 years ago

0509c9c6

chore(data/polynomial/ring_division): golf a few proofs (#14097)

urkud committed 3 years ago

c8edd608

chore(order/filter/basic): golf a few proofs (#14078)

urkud committed 3 years ago

6cf6e8cb

feat(data/polynomial/laurent): add truncation from Laurent polynomials to polynomials (#14085)

adomani committed 3 years ago

9b41e4e0

Newer Older