Commits leanprover-community/mathlib

feat(order/well_founded): typeclasses for well-founded `<` and `>` (#15399)

vihdzp committed 4 years ago

b3efc733

feat(data/nat/totient): lemmas `totient_mul_of_prime_of_{not_}dvd` (#15645)

stuart-presnell committed 4 years ago

b9387a48

feat(analysis/convex/cone): add inner_dual_cone_eq_Inter_inner_dual_cone_singleton (#15639)

apurvnakade committed 4 years ago

23c39818

feat(algebraic_topology/dold_kan): construction of idempotent endomorphisms (#15616)

joelriou committed 4 years ago

735943a2

feat(ring_theory/algebraic): `is_algebraic_algebra_map_iff` (#15586)

tb65536 committed 4 years ago

017e1f13

feat(linear_algebra/finite_dimensional): One-dimensional iff principal (#15558)

erdOne committed 4 years ago

e9d99674

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

samvang committed 4 years ago

a6f325fe

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

erdOne committed 4 years ago

b4f242f1

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

Paul-Lez committed 4 years ago

03172b6b

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

erdOne committed 4 years ago

f11e306a

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

Michael14071407 committed 4 years ago

42eb7f2d

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

TwoFX committed 4 years ago

061ea99a

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

tb65536 committed 4 years ago

8f26acee

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

huynhtrankhanh committed 4 years ago

bb3f990f

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

erdOne committed 4 years ago

ba9c8f35

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

erdOne committed 4 years ago

f746956a

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

erdOne committed 4 years ago

b8fb47c4

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

erdOne committed 4 years ago

01c60b26

feat(category_theory): full_of_surjective (#14974)

TwoFX committed 4 years ago

cffa0311

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

javra committed 4 years ago

293da933

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

TwoFX committed 4 years ago

b583055c

Super annoying timeout

ADedecker committed 4 years ago

3bd3af67

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 4 years ago

a0e2c623

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

leanprover-community-bot committed 4 years ago

a5f78c98

Induction is incredible

ADedecker committed 4 years ago

e7a0d977

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

ADedecker committed 4 years ago

8b14198b

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

YaelDillies committed 4 years ago

46b19752

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

ADedecker committed 4 years ago

10aeb392

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

vihdzp committed 4 years ago

8050ac7c

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

ADedecker committed 4 years ago

c6357eeb