leanprover-community/mathlib

Pull Requests Commits

Enhance using directedness

ADedecker committed 3 years ago

c6ccec08

ADedecker committed 3 years ago

5327da3f

ADedecker committed 3 years ago

f9dcfbe7

ADedecker committed 3 years ago

4bd619bd

Relation with `tendsto_uniformly`

ADedecker committed 3 years ago

bc2b3cb0

ADedecker committed 3 years ago

b04e3476

ADedecker committed 3 years ago

976551f2

ADedecker committed 3 years ago

6a209c7b

Defining an uniform_space by a uniformity basis

ADedecker committed 3 years ago

71e37add

feat(algebra/associates): add two instances and a lemma about the order on the monoid of associates of a monoid (#12863)

Paul-Lez committed 3 years ago

cdd1703c

fix(data/fintype/basic): generalize fintype instance for fintype.card_coe (#13055)

kmill committed 3 years ago

cd51f0de

chore(*): removing some `by { dunfold .., apply_instance }` proofs (#13050)

mcdoll committed 3 years ago

f2fd6db6

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

leanprover-community-bot committed 3 years ago

ca3bb9ef

feat(measure_theory/*): refactor integral to allow non second-countable target space (#12942)

sgouezel committed 3 years ago

fc758559

feat(linear_algebra/dual): define the algebraic dual pairing (#12827)

mcdoll committed 3 years ago

d28a163e

feat(algebra/ring/basic): neg_zero for distrib_neg (#13049)

ericrbg committed 3 years ago

c594e2b9

feat(set_theory/cardinal): bit lemmas for exponentiation (#13010)

vihdzp committed 3 years ago

b446c498

fix(tactic/norm_num): make norm_num user command match norm_num better (#12667)

kmill committed 3 years ago

92b29c77

feat(combinatorics/simple_graph/regularity/energy): Energy of a partition (#12958)

YaelDillies committed 3 years ago

523d1779

feat(algebra/algebra/unitization): define unitization of a non-unital algebra (#12601)

j-loreaux committed 3 years ago

50903f0d

chore(ring_theory/valuation/basic): fix valuation_apply (#13045)

mariainesdff committed 3 years ago

119eb05e

feat(algebra/module): `sub_mem_iff_left` and `sub_mem_iff_right` (#13043)

Vierkantor committed 3 years ago

e4c64493

feat(algebra/algebra/tower): `span A s = span R s` if `R → A` is surjective (#13042)

Vierkantor committed 3 years ago

9aec6df4

feat(category_theory/abelian): constructor in terms of coimage-image comparison (#12972)

kim-em committed 3 years ago

d3684bc3

feat(algebra/direct_sum/module): link `direct_sum.submodule_is_internal` to `is_compl` (#12671)

eric-wieser committed 3 years ago

e92ecffc

chore(analysis/normed_space/exponential): fix lemma names in docstrings (#13032)

eric-wieser committed 3 years ago

90f0bee6

chore(data/list/pairwise): add `pairwise_bind` (#13030)

eric-wieser committed 3 years ago

993d5764

chore(data/list): two lemmas about bind (#13029)

eric-wieser committed 3 years ago

89998136

feat(ring_theory/valuation/basic): add add_valuation.valuation (#12914)

mariainesdff committed 3 years ago

cedf0220

chore(topology/vector_bundle): fix timeout by optimizing proof (#13026)

Vierkantor committed 3 years ago

84b8b0d8

Older