Commits leanprover-community/mathlib3

feat(analysis/convolution): The convolution of two functions (#13540)

fpvandoorn committed 3 years ago

41ca6015

feat(analysis/complex/phragmen_lindelof): Phragmen-Lindelöf principle for some shapes (#13178)

urkud committed 3 years ago

baad0026

feat(model_theory/syntax, semantics): Lemmas about relabeling variables (#14225)

awainverse committed 3 years ago

1ccb7f04

feat(model_theory/satisfiability): Upward Löwenheim–Skolem (#13982)

awainverse committed 3 years ago

4b9e57b1

chore(filter/pointwise): protect filter.has_involutive_inv (#14398)

ericrbg committed 3 years ago

25f75c4e

chore(ring_theory/artinian): clarify left/right -ness in doc strings (#14396)

ocfnash committed 3 years ago

2a9b0f85

feat(algebraic_topology): the nerve of a category (#14304)

joelriou committed 3 years ago

841aef25

feat(category_theory/monoidal/subcategory): full monoidal subcategories (#14311)

antoinelab01 committed 3 years ago

bae02292

feat(order/bounded_order): define `with_bot.map` and `with_top.map` (#14163)

urkud committed 3 years ago

48d831a4

feat(combinatorics/simple_graph/connectivity): deleting edges outside a walk (#14110)

kmill committed 3 years ago

8dd4619b

feat(data/real/nnreal): add mul csupr/cinfi lemmas (#13936)

mariainesdff committed 3 years ago

27791f97

feat(order/rel_classes): Reflexive relation from irreflexive and viceversa (#13411)

vihdzp committed 3 years ago

525cc652

feat(logic/function/basic): add `function.const_injective` (#14388)

urkud committed 3 years ago

b2973b12

chore(data/stream/defs): add spaces around infix operators (#14386)

urkud committed 3 years ago

d3b155bb

chore(set_theory/ordinal/topology): add `variables` block (#14369)

vihdzp committed 3 years ago

034cf668

feat(topology/separation): split some proofs (#14337)

Ruben-VandeVelde committed 3 years ago

be34b950

feat(data/polynomial/*): `(p * q).trailing_degree = p.trailing_degree + q.trailing_degree` (#14384)

tb65536 committed 3 years ago

70e784d0

feat(algebra/order/monoid): add `le_iff_exists_mul'` (#14387)

urkud committed 3 years ago

5aeafaab

feat(order/succ_pred/interval_succ): new file (#14294)

urkud committed 3 years ago

acd05094

feat(category_theory/limits): products give pullback squares (#14327)

kim-em committed 3 years ago

4bf1b02f

feat(topology/continuous_function/stone_weierstrass): generalize the complex Stone-Weierstrass theorem to is_R_or_C fields (#14374)

dupuisf committed 3 years ago

634bef9f

refactor(data/polynomial/*): Make `support_C_mul_X_pow` match `support_monomial` (#14119)

tb65536 committed 3 years ago

c5b3de8d

feat(linear_algebra/prod): define the graph of a linear map (#14266)

ADedecker committed 3 years ago

dc0fadda

refactor(analysis/normed_space/M_structure): generalize to arbitrary faithful actions (#14222)

eric-wieser committed 3 years ago

fae32b6e

feat(data/polynomial/degree/trailing_degree): The trailing degree of a product is at least the sum of the trailing degrees (#14253)

tb65536 committed 3 years ago

189e5d13

move(group_theory/perm/cycle/*): A cycle folder (#14285)

YaelDillies committed 3 years ago

7e1c1263

feat(data/int/log): integer logarithms of linearly ordered fields (#13913)

eric-wieser committed 3 years ago

ba1c3f36

feat(topology/vector_bundle): use trivialization.symm to simplify the product of vector bundles (#14361)

fpvandoorn committed 3 years ago

f8d5c649

feat(measure_theory/function/conditional_expectation): Conditional expectation of an indicator (#14058)

RemyDegenne committed 3 years ago

660918bb

feat(measure_theory/integral): add formulas for average over an interval (#14132)

urkud committed 3 years ago

5da37314