leanprover-community/mathlib3

Pull Requests Commits

RemyDegenne committed 3 years ago

c8f50cde

Merge remote-tracking branch 'origin/master' into RD_subgaussian

RemyDegenne committed 3 years ago

424a04e4

feat(order/filter/bases): lemmas about bases of product filters (#15630)

urkud committed 3 years ago

8edffc25

chore(number_theory/padics/padic_integers): golf the comm_ring instance (#15590)

eric-wieser committed 3 years ago

671d57dc

feat(probability/moments): mgf/cgf of a sum of independent random variables (#15140)

RemyDegenne committed 3 years ago

e35aa928

feat(category_theory/limits): preserves biproducts if comparison is iso (#14419)

TwoFX committed 3 years ago

c4d273c2

feat(algebraic_topology/fundamental_groupoid): Define simply connected spaces (#12788)

prakol16 committed 3 years ago

38341f11

chore(analysis/inner_product_space): golf two proofs (#15679)

mcdoll committed 3 years ago

b21c9aa1

feat(order/filter/basic): add `filter.has_basis.bInter_mem` (#15661)

urkud committed 3 years ago

8fcb820b

feat(topology/basic): add lemmas about `filter.lift' _ closure` (#15653)

urkud committed 3 years ago

379b72c4

feat(tooplogy/metric_space/hausdorff_distance): add lemmas about `thickening` (#15641)

urkud committed 3 years ago

65d8b84e

chore(topology/locally_finite): move from `topology.basic` (#15640)

urkud committed 3 years ago

b08c7ace

feat(topology/separation): add `disjoint_nhds_nhds` (#15635)

urkud committed 3 years ago

2a9d5695

feat(topology/metric_space/lipschitz): add several lemmas (#15634)

urkud committed 3 years ago

d43aef06

feat(order/filter/*): `filter.pi` is countably generated (#15632)

urkud committed 3 years ago

a095eaeb

chore(algebra/jordan/basic): remove unused imports (#15686)

eric-wieser committed 3 years ago

4b76b9d6

refactor(category_theory/*): use simps in the old parts of the library (#14236)

kim-em committed 3 years ago

59382264

feat(algebra/jordan): Introduce Jordan rings (#11073)

mans0954 committed 3 years ago

edb7f923

doc(tactic/compute_degree): fix tactic tags, add examples to docs (#15680)

robertylewis committed 3 years ago

9d8c0f82

chore(scripts): update nolints.txt (#15685)

leanprover-community-bot committed 3 years ago

df09f2a7

feat(big_operators/fin): sum over elements of vector equal to `a` equals count `a` (#15360)

dtumad committed 3 years ago

1142e0b7

chore(tactic/fix_reflect_string): delete file (#15537)

hrmacbeth committed 3 years ago

d85af62f

feat(data/set/countable): add `iff` versions of some lemmas (#15671)

urkud committed 3 years ago

8da80f4e

feat(measure_theory/measure/finite_measure_weak_convergence): Add normalization of finite measures to probability measures and characterize weak convergence in terms of it. (#15528)

kkytola committed 3 years ago

f22fe49a

feat(algebra/lie/of_associative): add `commute.lie_eq` (#15675)

eric-wieser committed 3 years ago

fe45ef24

feat(data/sign): `left.sign_neg`, `right.sign_neg` (#15652)

jsm28 committed 3 years ago

c7ae1acf

refactor(measure_theory/function/uniform_integrable): change `uniform_integrable` to only require `ae_strongly_measurable` (#15623)

kex-y committed 3 years ago

287a69a0

feat(combinatorics/set_family/kleitman): Kleitman's bound (#14543)

YaelDillies committed 3 years ago

a6269fe6

feat(order/compare): general cleanup (#15665)

vihdzp committed 3 years ago

b877056e

feat(linear_algebra/annihilating_polynomial): add definition of annihilating ideal and show minpoly generates in field case (#12140)

twoquarterrican committed 3 years ago

98f0d695

Older