leanprover-community/mathlib3

Pull Requests Commits

feat(logic/nontrivial): function.injective.exists_ne (#3983)

jsm28 committed 5 years ago

1073204e

golf + add conversion lemmas

MadPidgeon committed 5 years ago

87f36eeb

pimsp committed 5 years ago

69d496c8

MadPidgeon committed 5 years ago

f690c6b2

feat(meta/widget): Add css classes for indentation as required by group and nest. (#3764)

DanielFabian committed 5 years ago

942c779d

Initial commit that actually type-checks

MadPidgeon committed 5 years ago

f0a20094

MadPidgeon committed 5 years ago

4572b186

Incorporate changes requested by TwoFX

pimsp committed 5 years ago

6d13f0cc

feat(data/complex/is_R_or_C): add typeclass for real or complex (#3934)

dupuisf committed 5 years ago

ffce8f67

feat(set_theory/game): computation of grundy_value (nim n + nim m) (#3977)

TwoFX committed 5 years ago

a18f142d

feat(data/fin): nontrivial instance (#3979)

jsm28 committed 5 years ago

dfdb38ab

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

pimsp committed 5 years ago

1d8443d1

Fixed linter problems

pimsp committed 5 years ago

22e2c29e

feat(linear_algebra/char_poly/coeff,*): prerequisites for friendship theorem (#3953)

jalex-stark committed 5 years ago

14e7fe83

feat(linear_algebra): determinant of vectors in a basis (#3919)

PatrickMassot committed 5 years ago

4c4243c5

Completed encoding of basic data types to strings for Turing machines

MadPidgeon committed 5 years ago

619ae734

Shortened proof of encodek_num

pimsp committed 5 years ago

f8121b1e

doc(topology/sheaves): update module docs (#3971)

kim-em committed 5 years ago

94b1292f

feat(data/nat): API for test_bit and bitwise operations (#3964)

TwoFX committed 5 years ago

ba41f0a4

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

pimsp committed 5 years ago

c6095748

Added documentation

pimsp committed 5 years ago

50c1d7d3

MadPidgeon committed 5 years ago

ced9d320

Fixed minor typo

pimsp committed 5 years ago

7abf2c69

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

pimsp committed 5 years ago

8e5408cd

Added unary encoding

pimsp committed 5 years ago

c328e769

MadPidgeon committed 5 years ago

ecc57cfe

chore(topology/sheaves/sheaf_of_functions): rely less on defeq (#3972)

kim-em committed 5 years ago

faf1df48

chore(*): bump to lean 3.19.0c, fin is now a subtype (#3955)

jcommelin committed 5 years ago

fd4628f1

Fixed merge conflicts

pimsp committed 5 years ago

1947bbc3

pimsp committed 5 years ago

acdc3602

Newer Older