leanprover-community/mathlib

Pull Requests Commits

feat(linear_algebra/bilinear_form): introduce adjoints of linear maps (#2746)

Oliver Nash committed 6 years ago

fa371f7b

feat(category_theory): show an epi regular mono is an iso (#2781)

b-mehta committed 6 years ago

315ba3e3

refactor(*iterate*): move to `function`; renamings (#2832)

urkud committed 6 years ago

efb4e959

feat(src/ring_theory): in a PID, all fractional ideals are invertible (#2826)

Vierkantor committed 6 years ago

19883648

feat(category_theory/abelian): abelian categories (#2817)

TwoFX committed 6 years ago

c812ebeb

feat(algebra/continued_fractions): add computation definitions and basic translation lemmas (#2797)

kappelmann committed 6 years ago

2deb6b46

feat(data/nat/prime): eq_prime_pow_of_dvd_least_prime_pow (#2791)

kim-em committed 6 years ago

798c61ba

feat(CI): add -T100000 to the build step in CI (#2276)

kim-em committed 6 years ago

85f08ec8

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

leanprover-community-bot committed 6 years ago

7c5eab3c

feat(ring_theory/prod): ring homs to/from `R × S` (#2836)

urkud committed 6 years ago

a7063ecc

chore(data/equiv/basic): simplify some defs, add `coe` lemmas (#2835)

urkud committed 6 years ago

6ee3a47e

feat(computability/tm_to_partrec): partrec functions are TM-computable (#2792)

digama0 committed 6 years ago

2a48225a

chore(*): split long lines, unindent in namespaces (#2834)

urkud committed 6 years ago

0d6d0b0f

feat(ring_theory/fintype): in a finite nonzero_semiring, fintype.card (units R) < fintype.card R (#2793)

kim-em committed 6 years ago

2792c93a

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

leanprover-community-bot committed 6 years ago

63b8c52c

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

leanprover-community-bot committed 6 years ago

4dfd706f

feat(linear_algebra/quadratic_form): equivalence of quadratic forms (#2769)

jcommelin committed 6 years ago

4ca776ee

feat(data/nat/primes): lemmas about min_fac (#2790)

kim-em committed 6 years ago

9630eca8

perf(tactic/lint): speed up nolint attribute (#2828)

gebner committed 6 years ago

895f5689

chore(src/algebra/ordered_ring.lean): fix linting errors (#2827)

Vierkantor committed 6 years ago

1cf59fcc

feat(data/polynomial): eq_one_of_is_unit_of_monic (#2823)

ChrisHughes24 committed 6 years ago

7d864755

chore(algebra/free_monoid): use implicit args in `lift` (#2821)

urkud committed 6 years ago

099ffd38

feat(number_theory/primorial): Bound on the primorial function (#2701)

Smaug123 committed 6 years ago

fc790892

feat(tactic/push_cast): take list of extra simp lemmas (#2825)

robertylewis committed 6 years ago

2c40bd3f

feat(order/filter/basic): a local left inverse locally equals a local right inverse (#2808)

urkud committed 6 years ago

ab2e52e0

feat(order/filter/basic): add `eventually.curry` (#2807)

urkud committed 6 years ago

8c36b32f

feat(analysis/calculus/implicit): Implicit function theorem (#2749)

urkud committed 6 years ago

597946df

feat(ring_theory/algebra): more on restrict_scalars (#2445)

kim-em committed 6 years ago

b4d4d9aa

feat(algebra/group_with_zero): mul_self_mul_inv (#2795)

jsm28 committed 6 years ago

ea403b34

feat(data/nat/basic): with_bot lemmas (#2822)

ChrisHughes24 committed 6 years ago

1c265e26

Newer Older