leanprover-community/mathlib

Pull Requests Commits

awainverse committed 3 years ago

1a1f96ed

awainverse committed 3 years ago

b1b9754d

awainverse committed 3 years ago

d7cead16

awainverse committed 3 years ago

e5e831a7

awainverse committed 3 years ago

e08aeab1

awainverse committed 3 years ago

7bdb4141

feat(model_theory/*): Lemmas about satisfiability (#16546)

awainverse committed 3 years ago

b3951c65

feat(measure_theory/measurable_space): pi has measurable singletons (#16542)

ericrbg committed 3 years ago

9824a558

chore(probability/process): split `probability/stopping.lean` into three files, create `process` folder (#16521)

RemyDegenne committed 3 years ago

c41e1712

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

awainverse committed 3 years ago

b9cdce00

Merge remote-tracking branch 'origin/satisfiability_lemmas' into complete_type

awainverse committed 3 years ago

ced4f7e3

Older