leanprover-community/mathlib3

Pull Requests Commits
feat(logic/function): add inv_fun_neg
johoelzl committed 6 years ago
cbe2f617
feat(logic/function): add injective.ne
johoelzl committed 6 years ago
73db4c7c
feat(logic): add plift.down_inj
johoelzl committed 6 years ago
c819617b
feat(linear_algebra/multivariate_polynomial): relate total_degree to degrees, add, zero, mul
johoelzl committed 6 years ago
985445f6
feat(linear_algebra/multivariate_polynomial): add degrees
johoelzl committed 6 years ago
78fd58dd
feat(data/finsupp): relatie to_multiset to 0, +, single, card, map, prod, and to_finset
johoelzl committed 6 years ago
c2d8bc2d
feat(data/finsupp): add support_mul
johoelzl committed 6 years ago
857842d0
feat(data/multiset): add prod_smul
johoelzl committed 6 years ago
a77797f9
feat(data/finset): add multiset.count_sup
johoelzl committed 6 years ago
e9247457
feat(data/finset): add to_finset_smul
johoelzl committed 6 years ago
e07cac54
feat(algebra/group_power): smul and pow are monoid homs
johoelzl committed 6 years ago
f24b01be
feat(linear_algebra): add dim_sup_add_dim_inf_eq
johoelzl committed 6 years ago
32642e17
feat(tactic/fin_cases): case bashing on finset, list, and fintype hypotheses. (#775)
kim-em committed 6 years ago
f46f0a67
docs(extras/tactic_writing): add ``%%(reflect n)`` to the tactic writing guide (#786)
kim-em committed 6 years ago
6cd0341a
chore(topology): Splits topology.basic and topology.continuity (#785)
Patrick Massot committed 6 years ago
201413b9
feat(analysis/{specific_limits,infinite_sum}): Cauchy of geometric bound (#753)
sgouezel committed 6 years ago
10848687
feat(ring_theory/ideal_operations): Chinese Remainder Theorem (#774)
kckennylau committed 6 years ago
1f90e189
hopefully fixed for good this time
ChrisHughes24 committed 6 years ago
fb8001d6
fix properly
ChrisHughes24 committed 6 years ago
182b2a3f
fix build
ChrisHughes24 committed 6 years ago
a4cc8b72
fix build
ChrisHughes24 committed 6 years ago
a75d57cb
generalize norm to zsqrtd
ChrisHughes24 committed 6 years ago
8dcd0718
fix build
ChrisHughes24 committed 6 years ago
d98cae7f
changing names
ChrisHughes24 committed 6 years ago
5cbd7fa7
The year is 2019
ChrisHughes24 committed 6 years ago
a9dfabac
put sum_two_squares in nat.prime namespace
ChrisHughes24 committed 6 years ago
c36470f7
move lemmas to correct places
ChrisHughes24 committed 6 years ago
d8f0921a
fix build
ChrisHughes24 committed 6 years ago
4e48324b
finish proof of sum two squares
ChrisHughes24 committed 6 years ago
9c9aee45
commit properly
ChrisHughes24 committed 6 years ago
bd86c0da
Terms Of Use Privacy Policy Refund Policy Impressum