leanprover-community/mathlib

Pull Requests Commits

remove variables, put them in the lemma

RemyDegenne committed 3 years ago

7b7bf239

RemyDegenne committed 3 years ago

98e433e8

RemyDegenne committed 3 years ago

69a8b594

RemyDegenne committed 3 years ago

36e194bd

restore instance attribute

RemyDegenne committed 3 years ago

7ea9c7c0

restore protected attribute

RemyDegenne committed 3 years ago

c251f787

exists_set_sigma_finite

RemyDegenne committed 3 years ago

d0e3a038

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

stuart-presnell committed 3 years ago

b9387a48

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

apurvnakade committed 3 years ago

23c39818

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

joelriou committed 3 years ago

735943a2

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

tb65536 committed 3 years ago

017e1f13

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

erdOne committed 3 years ago

e9d99674

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

Older