Commits leanprover-community/mathlib3

refactor(topology/sheaves): Redefine sheaves in terms of Grothendieck topology. (#15384)

erdOne committed 3 years ago

b8fb47c4

feat(ring_theory/ring_hom/finite): Finite type is a local property (#15379)

erdOne committed 3 years ago

01c60b26

feat(category_theory): full_of_surjective (#14974)

TwoFX committed 3 years ago

cffa0311

feat(ring_theory): the Ore localization of a ring (#14348)

javra committed 3 years ago

293da933

feat(category_theory): a category with a small detecting set is well-powered (#15238)

TwoFX committed 3 years ago

b583055c

refactor(topology/algebra/order/basic): Add antitone versions of sup and inf lemmas for continuous monotone functions and move them to monotone/antitone namespaces. (#15218)

kkytola committed 3 years ago

a0e2c623

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

leanprover-community-bot committed 3 years ago

a5f78c98

refactor(algebra/big_operators/basic): Use `to_additive` (#15702)

YaelDillies committed 3 years ago

46b19752

style(analysis/inner_product_space/l2_space): small style improvement (#15698)

ADedecker committed 3 years ago

10aeb392

feat(set_theory/zfc/basic): `inj` lemmas (#15545)

vihdzp committed 3 years ago

8050ac7c

feat(analysis/inner_product_space): in finite dimension, hilbert basis = orthonormal basis (#15540)

ADedecker committed 3 years ago

c6357eeb

chore(topology/sequences): drop local notation `x ⟶ a` (#15696)

urkud committed 3 years ago

f3e89fb4

chore(data/list/of_fn): injectivity (#15695)

eric-wieser committed 3 years ago

4a6e8cff

feat(analysis/inner_product/pi_L2): a finite orthonormal family is a basis of its span (#15481)

ADedecker committed 3 years ago

fc5a82e1

feat(set/intervals/monotone): add some monotonicity lemmas (#14896)

kex-y committed 3 years ago

eea396ef

chore(data/set/{function,countable}): extract a lemma from a proof (#15668)

urkud committed 3 years ago

fd77cbf2

feat(ring_theory/valuation/valuation_subring): define maximal ideal of valuation subring and provide basic API (#14656)

mckoen committed 3 years ago

8bc2354c

feat(measure_theory/constructions/borel_space): the set of points for which a measurable sequence of functions converges is measurable (#15307)

kex-y committed 3 years ago

70887f86

feat(measure_theory/function/conditional_expectation): pull-out property of the conditional expectation (#15274)

RemyDegenne committed 3 years ago

86f80202

feat(tactic/positivity): a tactic for proving positivity/nonnegativity (#15618)

hrmacbeth committed 3 years ago

e517862a

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