leanprover-community/mathlib3

Pull Requests Commits

first attempt (#16557)

jcommelin committed 3 years ago

2c283537

feat(ring_theory/polynomial/symmetric): restore `finset.powerset_len` version of `prod_X_sub_C_coeff` (#16424)

alreadydone committed 3 years ago

5a1949ef

feat(topology/instances/ennreal): diameter of intervals (#16556)

sgouezel committed 3 years ago

4f570405

chore(analysis,topology): replace `noncomputable theory` with `noncomputable` (#16552)

eric-wieser committed 3 years ago

0f6cb5cf

feat(group_theory/commutator): Add `commutator_element_self` (#16437)

tb65536 committed 3 years ago

876ef05e

refactor(topology/constructions): golf, add `@[simp]`/`iff` variants (#16539)

urkud committed 3 years ago

23f73fe0

feat(data/set/intervals/ord_connected): lemmas about `order_dual` etc (#16534)

urkud committed 3 years ago

dc7225b9

feat(data/real/cau_seq): define sup and inf (#16494)

eric-wieser committed 3 years ago

1e1ed069

refactor(topology/uniform_space/separated): drop `is_separated` (#16458)

urkud committed 3 years ago

5e0a67a5

feat(algebra/order/ring): `linear_ordered_comm_semiring` (#16456)

YaelDillies committed 3 years ago

f67a9dec

refactor(topology/algebra/with_zero_topology): review API, golf (#16359)

urkud committed 3 years ago

49a1e11a

feat(topology/algebra/ordered): add lemmas, golf (#16343)

urkud committed 3 years ago

5645e721

feat(analysis/complex/poincare_metric): new file (#14703)

urkud committed 3 years ago

2572a025

feat(group_theory/coset): Add `quotient_equiv_of_eq` (#16439)

tb65536 committed 3 years ago

9e4166e2

feat(analysis/inner_product_space/basic): `ext_inner_map` (#16388)

mapehe committed 3 years ago

03a31f84

feat(topology/homeomorph): add `homeomorph.Pi_congr_right` (#16527)

ADedecker committed 3 years ago

df6f6e24

feat(topology): is_open and is_closed in term of ∀ᶠ and ∃ᶠ (#16545)

PatrickMassot committed 3 years ago

2874e437

feat(probability/martingale/borel_cantelli): Lévy's generalized Borel-Cantelli (#16358)

kex-y committed 3 years ago

a0be6eeb

feat(archive/birthday): improve birthday problem (#16528)

ericrbg committed 3 years ago

26660ec5

doc(number_theory/legendre_symbol/jacobi_symbol): remove now spurious reference to 'subscript J' (#16541)

MichaelStollBayreuth committed 3 years ago

92aa8256

feat(measure_theory/integral): finiteness of lower Lebesgue integral (#16514)

mcdoll committed 3 years ago

6386d90a

chore(topology/constructions): deduplicate (#16505)

urkud committed 3 years ago

7934d39c

chore(algebra/order/nonneg): add a `distrib_lattice` instance (#16493)

eric-wieser committed 3 years ago

3d2c3ad9

chore(order/symm_diff): Generalize to co-Heyting algebras (#16282)

YaelDillies committed 3 years ago

9149ac02

feat(topology/separation): define `T₅` spaces (#16533)

urkud committed 3 years ago

5483f598

doc(order/filter/basic): fix notations in doc of filter.comap (#16530)

xroblot committed 3 years ago

df48af67

move(algebra/field_power): Put lemmas in the correct place (#16465)

YaelDillies committed 3 years ago

692e2a9b

docs(data/list/defs): fix `list.dedup` docstring (#16535)

kmill committed 3 years ago

a2c0f220

feat(number_theory): Dedekind-Kummer theorem (#15000)

Vierkantor committed 3 years ago

a35c79d0

chore(algebra/order/monoid_lemmas_zero_lt): remove redundant assumptions (#16524)

astrainfinita committed 3 years ago

6454d85d

Newer Older