leanprover-community/mathlib3

Pull Requests Commits

digama0 committed 5 years ago

a2512f27

docs(data/complex/exponential): docstring for de Moivre (#4242)

jcommelin committed 5 years ago

5eedf327

fix(.github/workflows/add_label_from_review.yml): fix label removal (#4240)

bryangingechen committed 5 years ago

02ca5e28

feat(category_theory/monad/algebra): Add faithful instances. (#4227)

adamtopaz committed 5 years ago

d6707462

feat(field_theory): intermediate fields (#4181)

Vierkantor committed 5 years ago

5c31dea2

feat(ring_theory/polynomial): decomposing the kernel of an endomorphism polynomial (#4174)

abentkamp committed 5 years ago

e23b97e5

feat(category_theory/limits/creates): Add has_(co)limit defs (#4239)

adamtopaz committed 5 years ago

03894dff

chore(data/mv_polynomial): aeval_rename -> aeval_id_rename (#4230)

jcommelin committed 5 years ago

03775fbb

fix(data/mv_polynomial): fix doc strings (#4219)

shingtaklam1324 committed 5 years ago

3484e8be

refactor(measure_theory/simple_func_dense): split monolithic proof (#4199)

urkud committed 5 years ago

f0713cb9

feat(logic/embedding): use simps (#4169)

fpvandoorn committed 5 years ago

ba8fa0f1

chore(*): cleanup imports, split off data/finset/preimage from data/set/finite (#4221)

kim-em committed 5 years ago

5e934cd9

feat(data/mv_polynomial/rename): coeff_rename (#4203)

jcommelin committed 5 years ago

ed07cac5

feat(linear_algebra/eigenspace): generalized eigenvectors span the entire space (#4111)

abentkamp committed 5 years ago

ef18740b

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

leanprover-community-bot committed 5 years ago

4e414458

refactor(category_theory): make `has_image` and friends a Prop (#4195)

TwoFX committed 5 years ago

6b35819b

feat(data/(lazy_)list): various lemmas and definitions (#4172)

cipher1024 committed 5 years ago

96e81faa

feat(data/real/irrational): add a different formulation for irrationality (#4213)

jjaassoonn committed 5 years ago

69279580

feat(geometry/manifold): bundled smooth map (#3904)

Nicknamen committed 5 years ago

9aeffa83

feat(measure_theory): ext lemmas for measures (#3895)

fpvandoorn committed 5 years ago

72e5b9fc

fix(archive/100-thms): update link to 100.yaml in README (#4224)

bryangingechen committed 5 years ago

7cf8fa62

feat(data/polynomial/*): higher order derivative (#4187)

jjaassoonn committed 5 years ago

ecd889a5

feat(analysis/special_functions/trigonometric): continuity and differentiability of arctan (#4138)

hrmacbeth committed 5 years ago

5ab7eb0f

doc(data/list/tfae): Add skeletal docstring (#4220)

eric-wieser committed 5 years ago

d7aada16

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

leanprover-community-bot committed 5 years ago

937199ad

feat(archive/imo/*): add IMO 1972 B2, move IMOs to a subdirectory (#4209)

Stanislas Polu committed 5 years ago

392d3e37

feat(ring_theory/ideal/basic): mem_bot (#4211)

jcommelin committed 5 years ago

994c31d0

chore(data/mv_polynomial): Rename variables (#4208)

shingtaklam1324 committed 5 years ago

f2458d6f

refactor(ring_theory/algebra): re-bundle `subalgebra` (#4180)

Vierkantor committed 5 years ago

516b0dfd

feat(category_theory/monoidal): transport monoidal structure along an equivalence (#4123)

kim-em committed 5 years ago

d09ef4ab

Older