Commits leanprover-community/mathlib

feat(category_theory): construction of the localized category (#14422)

joelriou committed 3 years ago

350a3817

feat(category_theory/limits/shapes/comm_sq): opposites of is_pullback and is_pushout (#15269)

joelriou committed 3 years ago

00e7ca52

feat(topology/subset_properties): `locally_compact_space` instance for `Π` types (#15707)

ralvrz committed 3 years ago

cd7b23d1

feat(algebraic_geometry/morphisms): Quasi-compact morphisms of schemes (#15436)

erdOne committed 3 years ago

805bb2d2

feat(combinatorics/additive/behrend): Behrend's lower bound on Roth numbers (#15327)

YaelDillies committed 3 years ago

594e8848

feat(analysis/special_functions/gaussian): formula for gaussian integrals (#15106)

sgouezel committed 3 years ago

732279dd

feat(probability/martingale): the discrete stochastic integral of a submartingale is a submartingale (#14909)

kex-y committed 3 years ago

3086d342

feat(category_theory): a characterization of separating objects (#14838)

TwoFX committed 3 years ago

583a7034

chore(data/polynomial/cancel_leads): golf using `compute_degree_le` (#14776)

adomani committed 3 years ago

08af4a31

chore(analysis/convex/cone): add trivial coercion lemmas (#15713)

eric-wieser committed 3 years ago

c59720b4

feat(analysis/special_functions/trigonometric/angle): equality of `cos` or `sin` (#15651)

jsm28 committed 3 years ago

63eb48be

doc(field_theory/splitting_field): update code example to reflect changes to diamond issues (#15620)

eric-wieser committed 3 years ago

45732987

feat(linear_algebra): lemmas on associatedness of determinants of linear maps (#15587)

Vierkantor committed 3 years ago

ac2addd1

feat(computability/ackermann): the Ackermann function isn't primitive recursive (#15505)

vihdzp committed 3 years ago

69654263

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

vihdzp committed 3 years ago

b3efc733

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