leanprover-community/mathlib

Pull Requests Commits

Update lint-style.py

eric-wieser committed 5 years ago

Verified 565e432d

Deliberately remove a copyright header to make the linter fail

eric-wieser committed 5 years ago

Verified 3171768a

ci(lint-style): adjust output to integrate with github

eric-wieser committed 5 years ago

Verified b7479c4d

feat(ring_theory/polynomial/chebyshev/defs): Chebyshev polynomials of the second kind (#5793)

Julian-Kuelshammer committed 5 years ago

145f1270

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

leanprover-community-bot committed 5 years ago

1edd85c3

chore(data/fintype/basic): Remove duplicate instance (#5943)

eric-wieser committed 5 years ago

4dca6e1a

chore(combinatorics/simple_graph): generalise decidability proofs (#5938)

b-mehta committed 5 years ago

69e7f143

feat(data/list/basic): add diff_erase (#5941)

fpvandoorn committed 5 years ago

2cbaa9cc

chore(data/sym2): golf decidability proofs (#5940)

b-mehta committed 5 years ago

28702123

refactor(analysis/calculus/inverse): inverse of C^k functions over R or C (#5926)

sgouezel committed 5 years ago

645dc60f

fix(data/dfinsupp): fix overly strict type-class arguments (#5935)

eric-wieser committed 5 years ago

c43c709f

feat(analysis/normed_space/inner_product): existence of orthonormal basis (#5734)

hrmacbeth committed 5 years ago

82481e30

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

leanprover-community-bot committed 5 years ago

95454452

feat(archive/imo): formalize IMO 2013 problem Q5 (#5787)

dwrensha committed 5 years ago

6585eff9

feat(ring_theory/nullstellensatz): Classical Nullstellensatz (#5760)

dtumad committed 5 years ago

3e599600

refactor(data/set/basic): simpler proofs (#5920)

digama0 committed 5 years ago

4cc0d525

feat(data/fintype/basic): make subtype_of_fintype computable (#5919)

pechersky committed 5 years ago

8af7e08e

feat(algebra/*,linear_algebra/basic,ring_theory/ideal): lemmas about span of finite subsets and nontrivial maximal ideals (#5641)

Vierkantor committed 5 years ago

f45dee43

feat(data/zsqrtd/to_real): Add `to_real` (#5640)

eric-wieser committed 5 years ago

32fdb81b

feat(algebra/continued_fractions): add termination iff rat lemmas (#4867)

kappelmann committed 5 years ago

1011601d

feat(order/ideal): add partial_order instance to order.ideal (#5909)

mguaypaq committed 5 years ago

9adf9bb6

refactor(topology/local_homeomorph): simpler proof of `prod_symm` (#5906)

Jesse Michael Han committed 5 years ago

7244b43c

refactor(computability/primrec): simpler proof of `primrec.of_equiv` (#5905)

Jesse Michael Han committed 5 years ago

a859f10d

refactor(data/set/basic): simpler proof of `union_subset_iff` (#5904)

Jesse Michael Han committed 5 years ago

35638edb

chore(*): bump to lean-3.26.0 (#5895)

jcommelin committed 5 years ago

c64aa132

feat(measure_theory/independence): define independence of sets of sets, measurable spaces, sets, functions (#5848)

RemyDegenne committed 5 years ago

78a518a3

refactor(category_theory/abelian): golf `mono_of_kernel_ι_eq_zero` (#5914)

Jesse Michael Han committed 5 years ago

e5f9409c

refactor(data/complex/exponential): simplify proof of `tan_eq_sin_div_cos` (#5913)

Jesse Michael Han committed 5 years ago

1688b3e8

refactor(data/holor): simp -> refl (#5912)

Jesse Michael Han committed 5 years ago

e927930c

refactor(algebra/category/Group/limits): simp -> refl (#5911)

Jesse Michael Han committed 5 years ago

38f6e050

Older