leanprover-community/mathlib

Pull Requests Commits

This goal looks bad

jcommelin committed 5 years ago

ad46491b

Remove some sorries

jcommelin committed 5 years ago

23c2b193

kim-em committed 5 years ago

e03f9d0e

kim-em committed 5 years ago

0e512fe5

kim-em committed 5 years ago

fde1d183

kim-em committed 5 years ago

de45f273

kim-em committed 5 years ago

8a01c352

jcommelin committed 5 years ago

dbe74dab

Remove another sorry

jcommelin committed 5 years ago

601f4de7

Merge branch 'cayley_hamilton' of https://github.com/leanprover-community/mathlib into cayley_hamilton

jalex-stark committed 5 years ago

febd03e9

closed more sorries

jalex-stark committed 5 years ago

355a925b

characteristic_matrix_apply

jcommelin committed 5 years ago

98cd7801

Merge branch 'cayley_hamilton' of https://github.com/leanprover-community/mathlib into cayley_hamilton

jalex-stark committed 5 years ago

5efcaa0f

added an instance to close a sorry by apply_instance

jalex-stark committed 5 years ago

af76f7f9

jcommelin committed 5 years ago

4e1006c9

okay, that's the last of the bad ones

kim-em committed 5 years ago

0fb3e9f5

only two lemmas where there could possibly be dragons

kim-em committed 5 years ago

81e46868

one step closer

kim-em committed 5 years ago

0ffbc79e

kim-em committed 5 years ago

76c6de11

kim-em committed 5 years ago

f3370de4

kim-em committed 5 years ago

f1af63d7

migrate nonzero

kim-em committed 5 years ago

be9dae69

kim-em committed 5 years ago

a7c2d86f

kim-em committed 5 years ago

36094ece

kim-em committed 5 years ago

460c8758

kim-em committed 5 years ago

314bf1b5

kim-em committed 5 years ago

81038846

migrating stuff upwards

kim-em committed 5 years ago

d9606d93

extract out the algebra_map definition when setting up algebra k (monoid_algebra k G)

kim-em committed 5 years ago

a8a616c5

downgrade polynomial.C to a ring_hom

kim-em committed 5 years ago

69931acf

Older