leanprover-community/mathlib3

Pull Requests Commits

Merge branch 'master' into array

kim-em committed 6 years ago

Verified 9e312e29

fix(algebraic_geometry/presheafedspace): fix lame proofs (#1273)

kim-em committed 6 years ago

879da1cf

feat(tactic/interactive): move `rotate` into interactive namespace (#1272)

jesse-michael-han committed 6 years ago

9689f4d5

doc(contribute/index.md): add line about large PRs [ci skip] (#1267)

robertylewis committed 6 years ago

Verified d5a53939

feat(algebra/group/basic): add_add_neg_cancel'_right (#1261)

ChrisHughes24 committed 6 years ago

03c0d6c0

doc(contribute/style.md): fix section on comments [ci skip] (#1265)

robertylewis committed 6 years ago

Verified 926467dc

doc(*): new documentation requirements (#1229)

robertylewis committed 6 years ago

1000ae8d

feat(data/matrix): smul_val (#1262)

ChrisHughes24 committed 6 years ago

5125f11a

feat(category_theory): functions to convert is_lawful_functor and is_… (#1258)

johoelzl committed 6 years ago

ed579163

cleanup(category_theory/monoidal): use equiv on prod/punit intead of adding new constants (#1257)

johoelzl committed 6 years ago

b0c52519

feat(data/array): add some simp attributes (#1255)

ChrisHughes24 committed 6 years ago

4a5529a2

feat(linear_algebra/dim): findim equivalence (#1217)

abentkamp committed 6 years ago

a33315d5

feat(linear_algebra/finite_dimensional): finite dimensional vector spaces (#1241)

ChrisHughes24 committed 6 years ago

3e77fec2

feat(data/power_series): Add multivariate power series and prove basic API (#1244)

jcommelin committed 6 years ago

fd916604

feat(category_theory/*): define `Cat` and a fully faithful functor `Mon ⥤ Cat` (#1235)

urkud committed 6 years ago

7c09ed5e

chore(data/polynomial): clean up commented code (#1251)

jcommelin committed 6 years ago

b5a641e8

feat(logic/unique): forall_iff and exists_iff (#1249)

ChrisHughes24 committed 6 years ago

f24dc98b

refactor(ring_theory/noetherian): change order of instance arguments (#1250)

ChrisHughes24 committed 6 years ago

a8c29236

chore(data/equiv/algebra): add `ring.to_mul/add_equiv`, DRY (#1247)

urkud committed 6 years ago

93419b38

fix(group_theory/subgroup): fix some typos introduced in 66a86ffe0 (#1246)

urkud committed 6 years ago

d371da68

feat(category_theory/monad): monadic adjunctions (#1176)

kim-em committed 6 years ago

6e3516de

fix(data/matrix): use pi.module for the module structure (#1242)

ChrisHughes24 committed 6 years ago

9505e5b3

refactor(algebra/*): delete `free_monoid` from `algebra/free`, restore some functions in `algebra/group/with_one` (#1227)

urkud committed 6 years ago

07ae80f4

feat(analysis/calculus/times_cont_diff): multiple differentiability (#1226)

sgouezel committed 6 years ago

74754acb

feat(topology/algebra/group): define filter pointwise addition (#1215)

Zhouhang Zhou committed 6 years ago

8b102eb2

fix(data/{nat,int}/parity): fix definition of 'even' (#1240)

avigad committed 6 years ago

e704f940

fix(data/zmod/basic) remove unused argument from instance (#1239)

ChrisHughes24 committed 6 years ago

Verified 86e72876

feat(*): add nat.antidiagonal and use it for polynomial.mul_coeff (#1237)

jcommelin committed 6 years ago

d6fd044c

refactor(data/multiset): rename diagonal to antidiagonal (#1236)

jcommelin committed 6 years ago

8785bd0f

feat(data/mv_polynomial): coeff_mul (#1216)

jcommelin committed 6 years ago

e186fbb7

Older