leanprover-community/mathlib3

Pull Requests Commits

b-mehta committed 3 years ago

68d9cf66

b-mehta committed 3 years ago

ce72c507

doc(metric_space/basic): modify doc for metric spaces adding pseudo metric spaces (#16577)

faenuccio committed 3 years ago

0e18561d

feat(algebra/field/opposite): Missing instances (#16564)

YaelDillies committed 3 years ago

ea5af7d3

feat(algebra/order/hom/basic): `positivity` extension for nonnegative homs (#16228)

YaelDillies committed 3 years ago

2943d6ed

feat(topology/constructions): add/golf lemmas about `sigma` (#16571)

urkud committed 3 years ago

faeff0bb

feat(topology/algebra/mul_action): `add_torsor.connected_space` (#16471)

jsm28 committed 3 years ago

bc0344f3

feat(analysis/seminorm): continuity criterion for seminorms (#16402)

ADedecker committed 3 years ago

f69ae5ea

feat(linear_algebra/affine_space/affine_subspace): `affine_subspace.subtype` (#16372)

jsm28 committed 3 years ago

b898874f

feat(ring_theory/graded_algebra/basic): lemmas about rings graded by canonically ordered monoids (#16083)

jjaassoonn committed 3 years ago

f1d0841e

feat(algebra/hom/centroid): Introduce the centroid of a (non-unital, non-associative) semiring (#12746)

YaelDillies committed 3 years ago

4f2e9562

feat(topology/algebra/order): a linear order is T₅ (#16540)

urkud committed 3 years ago

511b9032

feat(order/bounded_order): distrib_lattice instances for with_top and with_bot (#16569)

eric-wieser committed 3 years ago

e2043de3

feat(group_theory/coset): Construct the embedding `H ⧸ ⨅ i, f i → Π i, H ⧸ f i` (#16560)

tb65536 committed 3 years ago

92d019a0

chore(topology/constructions): use `variables` (#16562)

urkud committed 3 years ago

48cffc51

feat(combinatorics/additive/pluennecke_ruzsa): The Plünnecke-Ruzsa inequality (#15440)

YaelDillies committed 3 years ago

b5e11670

feat(data/pfun): Product of partial functions (#15389)

YaelDillies committed 3 years ago

2125676c

feat(topology/uniform_space): Every Cauchy sequence over ℕ is totally bounded (#16563)

mcdoll committed 3 years ago

f7e0c81b

feat(measure_theory/measurable_space): add `prod.measurable_singleton_class` (#16559)

urkud committed 3 years ago

57f5c281

feat(model_theory/types): Complete types over a theory (#16548)

awainverse committed 3 years ago

65521b0a

refactor(data/real/basic): make `⊓` and `⊔` computable on reals (#16463)

eric-wieser committed 3 years ago

487385a4

feat(topology/separation): define `regular_space` (#16360)

urkud committed 3 years ago

92d989ce

feat(data/complex/module): get `smul_comm_class ℝ M E` from the one for `ℂ` (#16513)

j-loreaux committed 3 years ago

0ad279c1

feat(analysis/special_functions/compare_exp): new file (#16543)

urkud committed 3 years ago

857358a4

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

awainverse committed 3 years ago

c9046b8b

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

ericrbg committed 3 years ago

c91fbcc6

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

RemyDegenne committed 3 years ago

638d70a7

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

eric-wieser committed 3 years ago

5cec10d0

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

awainverse committed 3 years ago

51fbf041

Revert "first attempt (#16557)"

jcommelin committed 3 years ago

58c8f105

Older