leanprover-community/mathlib

Pull Requests Commits

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

chore(order/complete_lattice,data/set/lattice): move `Sup_sUnion` (#14077)

urkud committed 3 years ago

fa4c0368

feat(data/multiset/basic): `erase_singleton` (#14094)

alreadydone committed 3 years ago

bada932c

chore(set_theory/zfc): use `derive` for some instances (#14079)

urkud committed 3 years ago

55671bee

feat(algebra/*): Division monoid instances for `with_zero` and `mul_opposite` (#14073)

YaelDillies committed 3 years ago

d9e623c2

feat({data/{finset,set},order/filter}/pointwise): Pointwise monoids are division monoids (#13900)

YaelDillies committed 3 years ago

c57cfc6d

feat(data/polynomial/degree/definitions): if `r ≠ 0`, then `(monomial i r).nat_degree = i` (#14095)

adomani committed 3 years ago

c2e87de5

refactor(combinatorics/simple_graph/basic): relax `edge_finset` typeclasses (#14091)

kmill committed 3 years ago

59273305

feat(analysis/special_functions/pow): asymptotics for real powers and log (#14088)

b-mehta committed 3 years ago

41afd8c2

feat(data/complex): real exponential bounds (#14087)

b-mehta committed 3 years ago

1c8ce7e0

Newer Older