leanprover-community/mathlib3

Pull Requests Commits

b-mehta committed 3 years ago

e2642e2c

main statements

b-mehta committed 3 years ago

dc5068e0

b-mehta committed 3 years ago

67890488

Merge branch 'master' into bm-sharkovsky

b-mehta committed 3 years ago

712f93fb

b-mehta committed 3 years ago

6b505856

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

faenuccio committed 3 years ago

b1539919

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

YaelDillies committed 3 years ago

84b27545

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

YaelDillies committed 3 years ago

aae2a82f

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

urkud committed 3 years ago

d2057271

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

jsm28 committed 3 years ago

a6d28ae9

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

ADedecker committed 3 years ago

ae9b867e

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

jsm28 committed 3 years ago

e2ce3fa0

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

jjaassoonn committed 3 years ago

9936c3df

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

YaelDillies committed 3 years ago

30553f13

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

urkud committed 3 years ago

236a0af4

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

eric-wieser committed 3 years ago

a547b3b3

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

tb65536 committed 3 years ago

a5ed4088

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

urkud committed 3 years ago

b7cc093e

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

YaelDillies committed 3 years ago

4aab2abc

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

YaelDillies committed 3 years ago

744170a9

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

mcdoll committed 3 years ago

dc680a80

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

urkud committed 3 years ago

b76d2b40

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

awainverse committed 3 years ago

95d67152

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

eric-wieser committed 3 years ago

560891c4

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

urkud committed 3 years ago

0a67ddd4

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

j-loreaux committed 3 years ago

9019542b

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

urkud committed 3 years ago

ca827bae

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

Older