leanprover-community/mathlib

Pull Requests Commits

feat(number_theory): define "admissible" absolute values (#8964)

Vierkantor committed 4 years ago

ded0d640

feat(data/finset): define `finset.pimage` (#8907)

urkud committed 4 years ago

ec514603

chore(linear_algebra/basic): speed up slow decl (#9060)

jcommelin committed 4 years ago

628969b1

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

leanprover-community-bot committed 4 years ago

782a20a2

feat(algebra/algebra): lemmas connecting `basis ι R A`, `no_zero_smul_divisors R A` and `injective (algebra_map R A)` (#9039)

Vierkantor committed 4 years ago

dcd87822

docs(linear_algebra/bilinear_map): fix inconsistency in docstring (#9075)

jcommelin committed 4 years ago

50f5d8be

feat(data/int): absolute values and integers (#9028)

Vierkantor committed 4 years ago

b0b0a24f

chore(data/set/basic): add some simp attrs (#9074)

urkud committed 4 years ago

fd453cf1

feat(linear_algebra/finite_dimensional): generalisations to division_ring (#8822)

kim-em committed 4 years ago

463e7534

chore(ring_theory): typo fix (#9067)

Vierkantor committed 4 years ago

9c886ffb

feat(algebra/tropical/basic): define tropical semiring (#8864)

pechersky committed 4 years ago

f8cfed4d

feat(algebra/big_operators): absolute values and big operators (#9027)

Vierkantor committed 4 years ago

eeb4bb66

chore(linear_algebra/bilinear_map): split off new file from linear_algebra/tensor_product (#9054)

jcommelin committed 4 years ago

6c8203f2

feat(analysis/specific_limits): add `set.countable.exists_pos_has_sum_le` (#9052)

urkud committed 4 years ago

0508c7b1

feat(ring_theory): non-zero divisors are not zero (#9043)

Vierkantor committed 4 years ago

98942ab5

docs(algebra/ordered_ring): add module docstring (#9030)

YaelDillies committed 4 years ago

812ff38b

feat(algebra/algebra/subalgebra): inclusion map of subalgebras (#9013)

ChrisHughes24 committed 4 years ago

a84b538c

feat(ring_theory/ideal/local_ring): residue field is an algebra (#8991)

jcommelin committed 4 years ago

d69c12e9

doc(data/list/*): Add missing documentation (#8867)

BoltonBailey committed 4 years ago

58a88539

feat(ring_theory/ideal/operations): add some theorems about taking the quotient of a ring by a sum of ideals (#8668)

Paul-Lez committed 4 years ago

d366eb3d

feat(order/filter/basic): add `supr_inf_principal` and `tendsto_supr` (#9051)

urkud committed 4 years ago

d0c02bc9

chore(analysis/normed_space): add `dist_sum_sum_le` (#9049)

urkud committed 4 years ago

6b0c73a0

chore(data/bool): add a few lemmas about inequalities and `band`/`bor` (#9048)

urkud committed 4 years ago

3fdfc8e5

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

leanprover-community-bot committed 4 years ago

c4f37076

docs(set_theory/lists): add module docstring and def docstrings (#8967)

YaelDillies committed 4 years ago

77f4ed46

feat(topology/uniform_space/basic): add corollary of Lebesgue number lemma `lebesgue_number_of_compact_open` (#8963)

ocfnash committed 4 years ago

0c19d5f5

feat(data/matrix/hadamard): add the Hadamard product (#8956)

l534zhan committed 4 years ago

a7be93b2

feat(group_theory/subgroup): Normal Core (#8940)

tb65536 committed 4 years ago

91824e58

feat(*): trivial lemmas from #8903 (#8909)

urkud committed 4 years ago

298f231e

chore(linear_algebra/tensor_product): remove `@[ext]` tag from `tensor_product.mk_compr₂_inj` (#8868)

dupuisf committed 4 years ago

5b29630d

Newer Older