leanprover-community/mathlib

Pull Requests Commits

fix(ci): set GITHUB_TOKEN environment variable for gothub (#1920)

gebner committed 6 years ago

Verified b3683120

fix(ci): unshallow repo before pushing nightly tags (#1919)

gebner committed 6 years ago

99962ad7

chore(analysis/convex): move to `analysis/convex/basic` (#1918)

urkud committed 6 years ago

a948e313

fix(ci): work around github hack

gebner committed 6 years ago

e36d7ecc

fix(ci): try again to fix authentication

robertylewis committed 6 years ago

8e0d47ad

fix(scripts/deploy_nightly.sh): try to fix CI (#1917)

robertylewis committed 6 years ago

Verified 75743acb

chore(*): use filter.eventually (#1897)

gebner committed 6 years ago

cafd1937

feat(linear_algebra): Matrix inverses for square nonsingular matrices (#1816)

Vierkantor committed 6 years ago

bba84730

fix(.github/workflows/build): set pipefail (#1911)

gebner committed 6 years ago

5f015913

fix(archive/cubing_a_cube): roof broken by #1903 (#1912)

robertylewis committed 6 years ago

898cd708

feat(linear_algebra/matrix): define the trace of a square matrix (#1883)

Oliver Nash committed 6 years ago

497e692b

refactor(order/filter/basic): redefine `filter.pure` (#1889)

urkud committed 6 years ago

587b312e

feat(linear_algebra/multilinear): image of sum (#1908)

sgouezel committed 6 years ago

ce2e7a85

refactor(*): refactor `sum_smul`/`smul_sum` (#1910)

urkud committed 6 years ago

ab155ef9

feat(tactic/clear): add clear' tactic (#1899)

JLimperg committed 6 years ago

2297d200

feat(*): some simple lemmas about sets and finite sets (#1903)

urkud committed 6 years ago

9decec2b

feat(data/real/ereal): add `ereal` := [-oo,oo] (#1703)

kbuzzard committed 6 years ago

d3e5621d

fix(scripts/deploy_nightly): fill in blank env vars (#1909)

bryangingechen committed 6 years ago

d4aa088e

doc (analysis/normed_space/operator_norm): cleanup (#1906)

sgouezel committed 6 years ago

70772422

feat(topology/instances/ennreal): continuity of multiplication by const (#1905)

urkud committed 6 years ago

8c9a15eb

fix(scripts/deploy_nightly): token is now just the PAT, need to add user (#1907)

gebner committed 6 years ago

20f153a5

feat(data/real/nnreal): a few lemmas about subtraction (#1904)

urkud committed 6 years ago

3bbf8eb8

doc(geometry/manifold): fix markdown (#1901)

robertylewis committed 6 years ago

3b9ee8e8

fix(build): typo in deploy_nightly script name (#1902)

bryangingechen committed 6 years ago

d0756952

feat(.github): switch to github actions for ci (#1893)

gebner committed 6 years ago

2db02b80

feat(tactic/simp_rw): add `simp_rw` tactic, a mix of `simp` and `rw` (#1900)

Vierkantor committed 6 years ago

601d5b13

feat(order/filter/bases): define `filter.has_basis` (#1896)

urkud committed 6 years ago

69099f00

docs(data/mv_polynomial): add module docstring [ci skip] (#1892)

kbuzzard committed 6 years ago

aad853b5

feat(algebra/lie_algebra): define Lie subalgebras, morphisms, modules, submodules, quotients (#1835)

Oliver Nash committed 6 years ago

b686bc24

feat(order/filter/basic): prove `@cofinite ℕ = at_top` (#1888)

urkud committed 6 years ago

96ee2a69

Newer Older