leanprover-community/mathlib

Pull Requests Commits

feat(data/real/cau_seq): more lemmas about sup and inf (#16553)

eric-wieser committed 3 years ago

eb7d2664

feat(model_theory/satisfiability): Maximally consistent theories (#16547)

awainverse committed 3 years ago

043a74e2

Revert "first attempt (#16557)"

jcommelin committed 3 years ago

5ea93be0

first attempt (#16557)

jcommelin committed 3 years ago

Verified 1ae5da9d

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

alreadydone committed 3 years ago

d7e97106

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

sgouezel committed 3 years ago

d742555c

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

eric-wieser committed 3 years ago

3f498b03

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

tb65536 committed 3 years ago

dcf3c6b6

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

urkud committed 3 years ago

499ab570

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

urkud committed 3 years ago

77fa4dcf

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

eric-wieser committed 3 years ago

7cfeb2fa

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

urkud committed 3 years ago

e3fac0b5

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

YaelDillies committed 3 years ago

85c08a60

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

urkud committed 3 years ago

bb05277f

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

urkud committed 3 years ago

d673bafe

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

urkud committed 3 years ago

f59c26da

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

tb65536 committed 3 years ago

08899973

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

mapehe committed 3 years ago

7ec8f8a2

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

ADedecker committed 3 years ago

489bc58f

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

PatrickMassot committed 3 years ago

b4502fd1

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

kex-y committed 3 years ago

8c9342fd

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

ericrbg committed 3 years ago

827a83eb

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

MichaelStollBayreuth committed 3 years ago

7e74869c

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

mcdoll committed 3 years ago

1dc531a0

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

urkud committed 3 years ago

ba584a4c

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

eric-wieser committed 3 years ago

f8dfe810

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

YaelDillies committed 3 years ago

57bbd9ec

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

urkud committed 3 years ago

f7e477fd

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

xroblot committed 3 years ago

0ff46b9c

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

YaelDillies committed 3 years ago

a4f6c41e

Newer Older