leanprover-community/mathlib3

Pull Requests Commits

fun_like instances

dupuisf committed 3 years ago

a4ab437a

dupuisf committed 3 years ago

812bab87

Merge branch 'master' into dupuisf/continuous_functional_calculus_def

dupuisf committed 3 years ago

f681e5ed

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

feat(data/set/finite): set priority for fintype_insert' and document (#14363)

kmill committed 3 years ago

c1e21212

feat(group_theory/subgroup/basic): `zpowers_eq_bot` (#14366)

tb65536 committed 3 years ago

f5822984

chore(set_theory/surreal/basic): clarify some proofs (#14356)

Ruben-VandeVelde committed 3 years ago

ebb52066

refactor(analysis/normed_space/pi_Lp): golf some instances (#14339)

urkud committed 3 years ago

cdaa6d2b

fix(topology/vector_bundle): squeeze simp, remove non-terminal simp (#14357)

fpvandoorn committed 3 years ago

23f30a30

feat(topology/local_homeomorph): define helper definition (#14360)

fpvandoorn committed 3 years ago

88f8de36

Older