leanprover-community/mathlib3

Pull Requests Commits

Additional documentation for internal categories

z-murray committed 2 years ago

41879a16

Additional documentation for internal functors

z-murray committed 2 years ago

670f3acf

Removed internal_nat_trans_struct

z-murray committed 2 years ago

df4f12d2

Documentation for natural transformations

z-murray committed 2 years ago

d1312d76

z-murray committed 2 years ago

88084f7a

feat(category_theory): Internal categories, functors, and natural transformations

z-murray committed 2 years ago

7d9df50f

feat(category_theory/limits/shapes/pullbacks): Helpers for universal property and composition

z-murray committed 2 years ago

ccc256ef

feat(data/sum/basic): add some missing lemmas (#18184)

urkud committed 2 years ago

f4ecb599

chore(*): remove after the fact attribute [irreducible] at several places (2) (#18180)

sgouezel committed 2 years ago

39afa0b3

chore(*): remove after the fact `attribute [irreducible]` at several places (#18168)

sgouezel committed 2 years ago

565eb991

feat(ring_theory/ring_invo): add ring_invo_class (#18175)

LukasMias committed 2 years ago

ec2dfcae

chore(*): add mathlib4 synchronization comments (#18139)

leanprover-community-bot committed 2 years ago

f2f413b9

chore(*): sync `list.replicate` with Mathlib 4 (#18181)

urkud committed 2 years ago

47adfab3

feat(number_theory/divisors): add `nat.cons_self_proper_divisors` (#18176)

urkud committed 2 years ago

b13c1a07

feat(linear_algebra/basis): add basis.ext_elem_iff (#18155)

xroblot committed 2 years ago

f15389d9

refactor(*): define `list.replicate` and migrate to it (#18127)

urkud committed 2 years ago

f694c7de

feat(ring_theory/valuation/valuation_subring): Add `valuation_subring.inertia_subgroup` (#17086)

mkaratarakis committed 2 years ago

88b76e4c

feat(number_theory/diophantine_approximation): add new file proving Dirichlet's approximation theorem (#18019)

MichaelStollBayreuth committed 2 years ago

dc0f25ac

feat(algebra, linear_algebra): unique instances over the trivial ring (#18160)

alreadydone committed 2 years ago

dc17b6ac

feat(ring_theory/power_basis): minpoly_gen is always the minimal polynomial (#18117)

alreadydone committed 2 years ago

0a6c26ee

chore(archive/100-theorems-list/30_ballot_problem): golf (#18126)

urkud committed 2 years ago

761f9170

feat(ring_theory/polynomial/gauss_lemma): Prove Gauss's Lemma for integrally closed rings (#18147)

Paul-Lez committed 2 years ago

7a030ab8

chore(algebra/order/ring/canonical): use implicit variables (#18167)

riccardobrasca committed 2 years ago

a1b35592

fix(algebra/order/to_interval_mod): align `to_Ico_div` with regular division (#18105)

eric-wieser committed 2 years ago

a0ed43b3

chore(ring_theory/is_tensor_product): golf a slow proof (#18169)

eric-wieser committed 2 years ago

c4926d76

refactor(*): use `option.map₂` (#18081)

urkud committed 2 years ago

995b47e5

feat(analysis/normed/group/seminorm): add nonarchimedean (semi)norms (#17851)

mariainesdff committed 2 years ago

23c61a3c

chore(data/multiset/sort): make multiset repr a meta instance (#18163)

ChrisHughes24 committed 2 years ago

00638177

feat(data/part): add 2 lemmas (#18153)

urkud committed 2 years ago

80c43012

feat(order/bounds/basic): add `is_greatest_univ_iff` etc (#18162)

urkud committed 2 years ago

3310acfa

Older