Commits leanprover-community/mathlib

feat(algebraic_geometry): comap of surjective homomorphism is closed embedding (#15291)

samvang committed 3 years ago

a6f325fe

feat(ring_theory): Formally étale/smooth/unramified morphisms are stable under base change. (#15243)

erdOne committed 3 years ago

b4f242f1

chore(ring_theory/dedekind_domain/ideal): generalize a lemma (#15104)

Paul-Lez committed 3 years ago

03172b6b

feat(category_theory/limits/construction): Construct finite limits from terminal objects and pullbacks (#14948)

erdOne committed 3 years ago

f11e306a

feat(linear_algebra/basis): shows the lattice of submodules of a module over a division ring is atomistic (#14883)

Michael14071407 committed 3 years ago

42eb7f2d

feat(category_theory/preadditive): constructing a semiadditive structure from binary biproducts (#14445)

TwoFX committed 3 years ago

061ea99a

feat(group_theory/complement): transversal for the transfer homomorphism (#14182)

tb65536 committed 3 years ago

8f26acee

feat(data/sym/card): Prove stars and bars (#11162)

huynhtrankhanh committed 3 years ago

bb3f990f

feat(ring_theory/tensor_product): A predicate for being the tensor product. (#15512)

erdOne committed 3 years ago

ba9c8f35

feat(ring_theory/ring_hom/finite): Finite ring morphisms are stable under base change (#15427)

erdOne committed 3 years ago

f746956a

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

initial commit

kex-y committed 3 years ago

52692b77