leanprover-community/mathlib3

Pull Requests Commits

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

chore(algebra/algebra/unitization): update `comm_semiring` instance for `unitization` (#16048)

j-loreaux committed 3 years ago

63138639

feat(model_theory/syntax): Swapping between constants and variables (#14018)

awainverse committed 3 years ago

3baad3bf

feat(category_theory/limits): cone F ≌ costructured_arrow (const J) F (#15796)

TwoFX committed 3 years ago

8a032292

refactor(topology/constructions): review `quotient` API (#15986)

urkud committed 3 years ago

31800d81

refactor(category_theory/epi_mono): is_split_epi and split_epi (#16036)

joelriou committed 3 years ago

239d882c

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

leanprover-community-bot committed 3 years ago

b5b30b03

feat(probability/martingale/convergence): a.e. martingale convergence theorem (#15904)

kex-y committed 3 years ago

43e859a0

doc(ring_theory/valuation/valuation_subring): fix docstring (#16034)

kbuzzard committed 3 years ago

e1443c9c

Newer Older