leanprover-community/mathlib

Pull Requests Commits

move lemmas to better place

winstonyin committed 2 years ago

6f3d20d4

winstonyin committed 2 years ago

69338e9b

winstonyin committed 2 years ago

56077d9c

winstonyin committed 2 years ago

6f069033

winstonyin committed 2 years ago

1a6df678

winstonyin committed 3 years ago

56d4b862

Merge branch 'master' into integral_curve

ocfnash committed 3 years ago

f79fc9e2

feat(topology/subset_properties): upgrade `is_(pre)irreducible.closure` to iff (#17254)

alreadydone committed 3 years ago

226ea0fd

winstonyin committed 3 years ago

f0aee0cc

feat(measure_theory/measurable_space): add `measurable_of_countable` (#17266)

RemyDegenne committed 3 years ago

c5b46faa

winstonyin committed 3 years ago

db377d10

is_open_inter_of_mem

winstonyin committed 3 years ago

c4c089c5

feat(order/extension/well): Extend a well-founded order (#17054)

YaelDillies committed 3 years ago

65ee8572

feat(data/real/ennreal): Positivity extension for `ennreal.of_real` (#16955)

YaelDillies committed 3 years ago

1ab3ae03

feat(probability/borel_cantelli): the second Borel-Cantelli lemma (#16882)

kex-y committed 3 years ago

1e7dab97

refactor(data/fintype/basic): simplify the defeq of `sum.fintype` (#17236)

eric-wieser committed 3 years ago

e2b33abb

chore(combinatorics/quiver/path): reduce imports (#17216)

kim-em committed 3 years ago

88bad67d

doc(ring_theory/valuation/valuation_ring): Value "group" is a group with zero (#17210)

kbuzzard committed 3 years ago

31b18ef9

feat(tactic/positivity): Extension for `function.const` (#17126)

YaelDillies committed 3 years ago

e3bf3f11

feat(algebra/squarefree): x is squarefree iff (x) is radical in `gcd_monoid` (#17002)

alreadydone committed 3 years ago

79de90f7

feat(order/cover): Covering two distinct elements (#17274)

YaelDillies committed 3 years ago

b9cbf575

chore(analysis/complex/basic): golf some proofs (#17259)

eric-wieser committed 3 years ago

7c9a3b4b

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

leanprover-community-bot committed 3 years ago

ece3419a

feat(set_theory/cardinal): add `cardinal.range_nat_cast` (#17222)

urkud committed 3 years ago

a8a47a60

feat(algebra/order/upper_lower): Algebraic operations on upper sets (#16973)

YaelDillies committed 3 years ago

16279b04

feat(order/cover): add `wcovby_iff_le_and_eq_or_eq` (#17262)

eric-wieser committed 3 years ago

e0d82e89

feat(topology/continuous_on): add `tendsto_nhds_within_iff` (#17260)

RemyDegenne committed 3 years ago

34c828da

feat(group_theory/p_group): `card G = 1` or `p | card G`. (#17251)

tb65536 committed 3 years ago

1ee8921d

chore(data/finset/locally_finite): add more lemmas about one-sided intervals (#17033)

eric-wieser committed 3 years ago

bf07fdbb

docs(algebra/hom/group, tactic/push_neg): add docs to resolve some lint errors (#17225)

adomani committed 3 years ago

da8ded3f

Older