leanprover-community/mathlib

Pull Requests Commits

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

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

kmill committed 3 years ago

86a14674

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

Vierkantor committed 3 years ago

1e225257

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

astrainfinita committed 3 years ago

e763499b

doc(category/abelian/ext): update module doc (#16512)

kim-em committed 3 years ago

7a9e6ca4

feat(number_theory/legendre_symbol/norm_num): add file with `norm_num` extension for the Jacobi symbol (#16519)

MichaelStollBayreuth committed 3 years ago

8922aaa5

refactor(number_theory/padics/padic_val): make prime implicit (#15221)

Multramate committed 3 years ago

894c8c22

feat(linear_algebra/clifford_algebra/basic): lemmas about triple products of repeated vectors (#16153)

eric-wieser committed 3 years ago

d46774d4

feat(archive/100-theorems-list): Stirling, part 2 (#14875)

mo271 committed 3 years ago

fc35e1e9

feat(combinatorics/simple_graph/prod): add `locally_finite` instance for the box product of `locally_finite` graphs, plus two related lemmas (#16431)

bottine committed 3 years ago

104f141e

feat(linear_algebra/symplectic_group): add definition of symplectic group (#15513)

mpenciak committed 3 years ago

a5b382d8

Newer Older