Commits leanprover-community/mathlib

feat(order/filter/{basic, cofinite}, topology/subset_properties): filter lemmas, prereqs for #8611 (#9419)

hrmacbeth committed 4 years ago

d1f78e2e

chore({field,ring}_theory): generalize `fraction_ring` and `is_separable` to rings (#9415)

Vierkantor committed 4 years ago

f76d0198

chore(ring_theory/localization): speed up `localization` a bit (#9414)

Vierkantor committed 4 years ago

92526c89

refactor(data/mv_polynomial/equiv): simplify option_equiv_left (#9427)

ChrisHughes24 committed 4 years ago

8b238eb4

split(analysis/convex/jensen): split Jensen's inequalities off `analysis.convex.function` (#9445)

YaelDillies committed 4 years ago

c7dd27d7

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

leanprover-community-bot committed 4 years ago

d9ed0732

refactor(analysis/normed_space/{dual, pi_Lp}): split out inner product space parts (#9388)

hrmacbeth committed 4 years ago

f254c2f8

feat(topology/metric_space/basic): nonempty intersections of balls (#9448)

sgouezel committed 4 years ago

519ab351

chore(*): linting (#9343)

kim-em committed 4 years ago

acced829

split(analysis/convex/slope): split slope results off `analysis.convex.function` (#9444)

YaelDillies committed 4 years ago

3681b5a4

feat(data/real/ennreal): composition of coercion of natural numbers in ennreal (#9447)

sgouezel committed 4 years ago

eca3fd9a

feat(data/mv_polynomial/cardinal): cardinalities of polynomial rings (#9384)

ChrisHughes24 committed 4 years ago

88e613e7

feat(group_theory/sylow): Sylow's theorems for infinite groups (#9288)

tb65536 committed 4 years ago

2cd1d046

feat(linear_algebra/affine_space/combination, analysis/convex/combination): basic lemmas about affine combinations, center of mass, centroid (#9103)

ocfnash committed 4 years ago

9535c087

feat(analysis/convex/function): define strictly convex/concave functions (#9439)

YaelDillies committed 4 years ago

9e91b706

feat(data/mv_polynomial/basic): aeval_tower (#9429)

ChrisHughes24 committed 4 years ago

6f609baf

fix(linear_algebra/basic): generalize `linear_map.add_comm_group` to semilinear maps (#9402)

eric-wieser committed 4 years ago

43c1ab27

feat(ring_theory/algebraic): is_algebraic_of_larger_base_of_injective (#9433)

ChrisHughes24 committed 4 years ago

d2463aa3

chore(topology/sheaves): fix timeout by splitting proof (#9436)

Vierkantor committed 4 years ago

e1506687

feat(data/W/cardinal): results about cardinality of W-types (#9210)

ChrisHughes24 committed 4 years ago

0de54327

chore(analysis/convex/function): change `add_comm_monoid` to `add_comm_group` when carrier type is module of scalars containing -1 (#9442)

ocfnash committed 4 years ago

c758cec7

chore(analysis/normed_space/*): prereqs for #8611 (#9379)

hrmacbeth committed 4 years ago

d7abdff7

feat(measure_theory/measure/haar_lebesgue): properties of Haar measure on real vector spaces (#9325)

sgouezel committed 4 years ago

8bd75b26

chore(order/preorder_hom): more homs, golf a few proofs (#9256)

urkud committed 4 years ago

861d3bc4

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

leanprover-community-bot committed 4 years ago

49805e68

chore(data/fintype/basic): add `fintype.card_set` (#9434)

urkud committed 4 years ago

73afb6c7

feat(data/mv_polynomial/supported): subalgebra of polynomials supported by a set of variables (#9183)

ChrisHughes24 committed 4 years ago

e2cb9e19

feat(set_theory/continuum): define `cardinal.continuum := 2 ^ ω` (#9354)

urkud committed 4 years ago

e18b9cac

chore(order/*): replace `mono_incr` and `mono_decr` in lemma names wih `monotone` and `antitone` (#9428)

eric-wieser committed 4 years ago

15f15a6e

fix(algebra/opposites): add a missing `comm_semiring` instance (#9425)

eric-wieser committed 4 years ago

2d5fd655