leanprover-community/mathlib3

Pull Requests Commits

chore(data/matrix/basic): clean up of new lemmas on matrix numerals (#2996)

kim-em committed 5 years ago

24ce416a

feat(dynamics/fixed_points/topology): new file (#2991)

urkud committed 5 years ago

7bb2d89f

chore(scripts): update nolints.txt (#2993)

leanprover-community-bot committed 5 years ago

470ccd32

feat(data/real/conjugate_exponents): define real conjugate exponents (#2992)

sgouezel committed 5 years ago

94dedddf

chore(*): use prod notation (#2989)

kckennylau committed 5 years ago

4ee67acb

feat(geometry/euclidean): angles and some basic lemmas (#2865)

jsm28 committed 5 years ago

a377993a

feat(order/ideal): order ideals, cofinal sets and the Rasiowa-Sikorski lemma (#2850)

dwarn committed 5 years ago

dbbd696d

chore(*): add docs and nolints (#2990)

urkud committed 5 years ago

d204daa5

refactor(algebra/*): move `commute` below `ring` in `import`s (#2973)

urkud committed 5 years ago

9fba817f

feat(data/matrix/basic): add bit0, bit1 lemmas (#2987)

pechersky committed 5 years ago

2caf479d

chore(algebra/ordered_ring): use le instead of ge (#2986)

sgouezel committed 5 years ago

3ca4c270

feat(data/nat/digits): digits, and divisibility tests for Freek 85 (#2686)

kim-em committed 5 years ago

47f73356

feat(ring_theory/fractional_ideal): pushforward of fractional ideals (#2984)

Vierkantor committed 5 years ago

a7930425

feat(ring/localization): add fraction map for int to rat cast (#2921)

alexjbest committed 5 years ago

c360e01a

feat(dynamics/circle): define translation number of a lift of a circle homeo (#2974)

urkud committed 5 years ago

592f769e

ci(deploy_docs.sh): generalize for use in doc-gen CI (#2978)

bryangingechen committed 5 years ago

edd02097

fix(data/nat/basic): use protected attribute (#2976)

robertylewis committed 5 years ago

be21b9a4

chore(scripts): update nolints.txt (#2975)

leanprover-community-bot committed 5 years ago

516d9b54

chore(algebra/ring): fix docs, `def`/`lemma` (#2972)

urkud committed 5 years ago

a7f0069c

chore(topology/basic): remove unneeded `mk_protected` (#2971)

rwbarton committed 5 years ago

16ad1b41

feat(category_theory/eq_to_hom): functor extensionality using heq (#2712)

rwbarton committed 5 years ago

b59f777c

chore(analysis/normed_space/mazur_ulam): add `to_affine_map` (#2963)

urkud committed 5 years ago

2a36d256

chore(*): protect some definitions to get rid of _root_ (#2846)

jcommelin committed 5 years ago

a44c9a18

feat(data/padics/padic_norm): New padic_val_nat convenience functions (#2970)

Smaug123 committed 5 years ago

e48c2af4

feat(number_theory/lucas_lehmer): prime (2^127 - 1) (#2842)

kim-em committed 5 years ago

589bdb97

chore(algebra/group_with_zero_power): review (#2966)

urkud committed 5 years ago

ed5f6360

feat(analysis/convex/specific_functions): convexity of rpow (#2965)

sgouezel committed 5 years ago

2f028a88

fix(tactic/ring_exp): `ring_exp` now recognizes that `2^(n+1+1) = 2 * 2^(n+1)` (#2929)

Vierkantor committed 5 years ago

f096a74a

fix(documentation): fix a typo in the readme (#2969)

TwoFX committed 5 years ago

6f272716

chore(algebra/ordered_group): add `exists_pos_add_of_lt` (#2967)

urkud committed 5 years ago

d1ae307b

Newer Older