leanprover-community/mathlib3

Pull Requests Commits

feat(data/fintype): finset.univ_map_embedding (#2765)

kim-em committed 5 years ago

90abd3bb

feat(data/polynomial): prime_of_degree_eq_one_of_monic (#2745)

ChrisHughes24 committed 5 years ago

69485051

chore(data/equiv): make `equiv.ext` args use { } (#2776)

urkud committed 5 years ago

8c1793fe

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

leanprover-community-bot committed 5 years ago

f66caaad

feat(algebra/invertible): invertible_of_ring_char_not_dvd (#2775)

kim-em committed 5 years ago

c6aab262

feat(analysis/normed_space/banach): add `continuous_linear_equiv.of_bijective` (#2774)

urkud committed 5 years ago

58789f7d

refactor(ring_theory/localization): characterise ring localizations up to isomorphism (#2714)

101damnations committed 5 years ago

80ad9edc

chore(linear_algebra/projection): use implicit args in lemmas (#2773)

urkud committed 5 years ago

a012d76d

feat(category_theory): preadditive binary biproducts (#2747)

TwoFX committed 5 years ago

749e39fe

chore(linear_algebra/basic): redefine le on submodule (#2766)

ChrisHughes24 committed 5 years ago

5585e3cb

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

leanprover-community-bot committed 5 years ago

a9960cef

feat(analysis/normed_space): complemented subspaces (#2738)

urkud committed 5 years ago

6c71874b

fix(*): do not nolint simp_nf (#2734)

gebner committed 5 years ago

fd45e288

perf(tactic/lint/simp): speed up `simp_comm` linter (#2760)

gebner committed 5 years ago

ec01a0d5

feat(order/lattice): sup_left_idem and similar (#2768)

ChrisHughes24 committed 5 years ago

d532eb60

refactor(data/nat/basic): use function equality for `iterate` lemmas (#2748)

urkud committed 5 years ago

951b967d

chore(archive/sensitivity): Clean up function coercion in sensitivity proof (depends on #2756) (#2758)

PatrickMassot committed 5 years ago

a540d79b

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

leanprover-community-bot committed 5 years ago

3c9bf6b8

feat(ring_theory/principal_ideal_domain): definition of principal submodule (#2761)

Vierkantor committed 5 years ago

d6420bdc

feat(algebra): the R-module structure on S-linear maps, for S an R-algebra (#2759)

kim-em committed 5 years ago

4c3e1a9d

chore(*): update to Lean 3.14.0 (#2756)

PatrickMassot committed 5 years ago

6df77a61

chore(category_theory): attributes and a transport proof (#2751)

b-mehta committed 5 years ago

164c2e3c

feat(category_theory/binary_products): some product lemmas and their dual (#2752)

b-mehta committed 5 years ago

ab5d0f15

docs(linear_algebra/sesquilinear_form): correct module docs (#2757)

Vierkantor committed 5 years ago

1f002829

feat(linear_algebra/projection): projection to a subspace (#2739)

urkud committed 5 years ago

cbe80ed2

feat(data/nat/choose): sum_range_choose_halfway (#2688)

Smaug123 committed 5 years ago

3c1f9f9c

feat(logic/basic): spaces with a zero or a one are nonempty (#2743)

sgouezel committed 5 years ago

e3aca90a

feat(algebra/big_operators): reversing an interval doesn't change the product (#2740)

urkud committed 5 years ago

607767e2

fix(ci): replace 2 old secret names (#2744)

bryangingechen committed 5 years ago

62c22daf

chore(*): remove non-canonical `option.decidable_eq_none` instance (#2741)

gebner committed 5 years ago

1e185125

Newer Older