leanprover-community/mathlib

Pull Requests Commits

feat(combinatorics/simple_graph): add three useful lemmas relating walk.support and walk.append (#15687)

bottine committed 3 years ago

cdb7af2f

feat(analysis/seminorm): Group seminorms (#15594)

YaelDillies committed 3 years ago

fb1787b1

refactor(analysis/inner_product_space): rename `is_self_adjoint` to `is_symmetric` and add `is_self_adjoint` (#15326)

mcdoll committed 3 years ago

5c91a35b

feat(ring_theory/polynomial/vieta): add version of prod_X_add_C_eq_sum_esymm for multiset (#15008)

xroblot committed 3 years ago

05d8b4f3

feat(topology/uniform_space/uniform_convergence_topology): continuity of [pre,post]composition, and other topological properties (#14534)

ADedecker committed 3 years ago

f1e5c657

feat(algebraic_geometry/*): Preliminary lemmas for #16059 (#16060)

erdOne committed 3 years ago

34b2a989

feat(topology/algebra/uniform_group): add instance `topological_group_is_uniform_of_compact_space` (#16027)

ocfnash committed 3 years ago

531db2ef

feat(algebraic/dold_kan): construction of the functors N₁ and N₂ (#16003)

joelriou committed 3 years ago

07d11baa

feat(algebraic_geometry): Being quasi-compact is a local property. (#15995)

erdOne committed 3 years ago

9b298fea

chore(ring_theory/*): make ACC/DCC on rings be defeq to module versions (#15989)

ericrbg committed 3 years ago

13482743

feat(algebra/group_with_zero): generalize some lemmas (#15985)

urkud committed 3 years ago

9e25db49

chore(combinatorics/*): Fix lint (#16031)

YaelDillies committed 3 years ago

1e6b748c

chore(topology/*): Fix lint (#16030)

YaelDillies committed 3 years ago

1ec48762

feat(combinatorics/young_diagram): add Young diagrams (#15822)

jakelev committed 3 years ago

8a9a16da

feat(order/bounded_order): with_top.of_dual (#15727)

pechersky committed 3 years ago

091ccfb2

feat(catgory_theory/sites): Image sheaf (#15282)

erdOne committed 3 years ago

75edc28a

feat(group_theory/divisible): definition of divisible group (#15030)

jjaassoonn committed 3 years ago

445154a5

refactor(data/set/basic): Adds `inter_nonempty` to match `union_nonempty`. (#14854)

linesthatinterlace committed 3 years ago

8cd4f196

feat(category_theory/preadditive): inclusion functor from left exact functors to additive functors (#12339)

TwoFX committed 3 years ago

9f5d911e

feat(set/prod): decidable mem instance for diagonal (#15846)

dtumad committed 3 years ago

ed833060

chore(probability/martingale/convergence): fix doc-string (#16062)

kex-y committed 3 years ago

3cf22a91

chore(category_theory/limits): generalize universes for limits in punit (#16050)

TwoFX committed 3 years ago

c85d2ff9

feat(category_theory): `discrete punit` is filtered and cofiltered (#16045)

TwoFX committed 3 years ago

6b7e12a9

chore(data/polynomial/expand): update docstrings for move (#16044)

Ruben-VandeVelde committed 3 years ago

92b557b0

chore(ring_theory/chain_of_divisors): make some variables that can be infered implicit (#16039)

Paul-Lez committed 3 years ago

ecc542a5

feat(data/*): `unique` instances for `dfinsupp` and `direct_sum` (#16017)

alreadydone committed 3 years ago

ff996689

feat(*): bump to lean 3.46.0 (#15994)

vihdzp committed 3 years ago

c1b5d219

feat(order/conditionally_complete_lattice): add `with_top.supr_coe_eq_top` and `with_top.supr_coe_lt_top` (#15979)

j-loreaux committed 3 years ago

674ff195

feat(analysis/convex/topology): minimize import (#16052)

ADedecker committed 3 years ago

8df20db4

feat(analysis/normed_space/basic): change `homeomorph_unit_ball` to make it obviously smooth (#15980)

ocfnash committed 3 years ago

4a379da7

Newer Older