leanprover-community/mathlib3

Pull Requests Commits

Unknown committed 5 years ago

f4b1fd7c

Unknown committed 5 years ago

64f89077

Unknown committed 5 years ago

e8e92afe

Unknown committed 5 years ago

5f546064

Unknown committed 5 years ago

33c4fb11

cleanup charpoly and cofactor expansion

Unknown committed 6 years ago

ba129891

finish char_polynomial_aux

Unknown committed 6 years ago

22b65724

Unknown committed 6 years ago

a99faa47

Unknown committed 6 years ago

85e785e4

Unknown committed 6 years ago

0afe24f0

cofactor expansion: finishing proof and cleanup

Unknown committed 6 years ago

b51b7e04

cofactor expansion of determinant (WIP)

Unknown committed 6 years ago

7b2cb5ec

Unknown committed 6 years ago

fea0ec4a

Unknown committed 6 years ago

c5703fef

Unknown committed 6 years ago

e543e87e

Unknown committed 6 years ago

49d53a44

Merge remote-tracking branch 'origin/master' into henselian

Unknown committed 6 years ago

54011cce

cleanup charpoly

Unknown committed 6 years ago

319b22f0

feat(data/finset): define `finset.Ico.subset_iff` (#1574)

urkud committed 6 years ago

f52e952e

feat(topology/topological_fiber_bundle): topological fiber bundles (#1421)

sgouezel committed 6 years ago

a4bbbdea

feat(algebra/geom_sum): sum of a geom_series over an Ico (#1573)

urkud committed 6 years ago

d2d29ffd

fix(scripts): sanity_check -> lint [ci skip] (#1575)

fpvandoorn committed 6 years ago

0b660a9f

feat(topology/metric_space): polygonal version of the triangle inequality (#1572)

urkud committed 6 years ago

809276c0

feat(meta/rb_map,tactic/monotonicity): replace rb_map.insert_cons (#1571)

robertylewis committed 6 years ago

b1654df1

feat(tactic/suggest): generalize and reimplement library_search (#1552)

Lucas Allen committed 6 years ago

74bed0c9

feat(algebra/big_operators): products and sums over `finset.Ico` (#1567)

urkud committed 6 years ago

f5446325

feat(tactic/lint): rename and refactor sanity_check (#1556)

robertylewis committed 6 years ago

173e70a0

feat(algebra/floor): prove `⌈x⌉ ≤ ⌊x⌋ + 1` (#1568)

urkud committed 6 years ago

ee398b66

chore(category_theory): using simps (#1500)

kim-em committed 6 years ago

05102ecb

feat(category_theory): def `is_isomorphic_setoid`, `groupoid.iso_equiv_hom` (#1506)

urkud committed 6 years ago

a1c0ad58

Older