leanprover-community/mathlib

Pull Requests Commits

feat(field_theory/polynomial_galois_group): New file (#5861)

tb65536 committed 4 years ago

e8e05265

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

eric-wieser committed 4 years ago

62cf420b

doc(algebra/polynomial/big_operators): add / fix docstrings and lint (#5950)

bryangingechen committed 4 years ago

657cfeb6

feat(analysis/normed_space/inner_product): existence of isometry to Euclidean space (#5949)

hrmacbeth committed 4 years ago

aabb8436

chore(analysis/normed_space/multilinear): rename variables (#5929)

urkud committed 4 years ago

0d18179a

chore(linear_algebra/linear_independent): relax requirements to semiring and division_ring (#5953)

eric-wieser committed 4 years ago

9c5064cc

fix(scripts): fix mixing absolute and relative paths to the linter (#5810)

Julian committed 4 years ago

783e11a5

chore(combinatorics/simple_graph/basic): remove classical locale (#5951)

kmill committed 4 years ago

41decdb1

refactor(topology/local_homeomorph): simplify `prod_trans` (#5915)

Jesse Michael Han committed 4 years ago

15217c2c

refactor(data/real/nnreal): shorter proof of `div_lt_iff` (#5945)

Jesse Michael Han committed 4 years ago

bbec0991

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

Julian-Kuelshammer committed 4 years ago

145f1270

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

leanprover-community-bot committed 4 years ago

1edd85c3

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

eric-wieser committed 4 years ago

4dca6e1a

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

b-mehta committed 4 years ago

69e7f143

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

fpvandoorn committed 4 years ago

2cbaa9cc

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

b-mehta committed 4 years ago

28702123

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

sgouezel committed 4 years ago

645dc60f

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

eric-wieser committed 4 years ago

c43c709f

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

hrmacbeth committed 4 years ago

82481e30

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

leanprover-community-bot committed 4 years ago

95454452

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

dwrensha committed 4 years ago

6585eff9

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

dtumad committed 4 years ago

3e599600

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

digama0 committed 4 years ago

4cc0d525

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

pechersky committed 4 years ago

8af7e08e

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

Vierkantor committed 4 years ago

f45dee43

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

eric-wieser committed 4 years ago

32fdb81b

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

kappelmann committed 4 years ago

1011601d

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

mguaypaq committed 4 years ago

9adf9bb6

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

Jesse Michael Han committed 4 years ago

7244b43c

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

Jesse Michael Han committed 4 years ago

a859f10d

Newer Older