Commits leanprover-community/mathlib

wip

eric-wieser committed 3 years ago

a262e9c0

feat(order/fractional_digits): digits of a linearly ordered field

eric-wieser committed 3 years ago

cbbf447c

feat(data/finset/n_ary): Binary image of finsets (#13718)

YaelDillies committed 3 years ago

ca1551c2

feat(analysis/normed_space/exponential): `Aeᴮ = eᴮA` if `AB = BA` (#13881)

eric-wieser committed 3 years ago

17412076

feat(data/zmod/basic): Generalize `zmod.card` (#13887)

tb65536 committed 3 years ago

c44091fc

feat(measure/function/l*_space): a sample of useful lemmas on L^p spaces (#13823)

sgouezel committed 3 years ago

2b0aeda1

docs(set_theory/game/pgame): Fix note on `pgame` (#13880)

vihdzp committed 3 years ago

aa921ef3

feat(set_theory/game/pgame): Negative of `of_lists` (#13868)

vihdzp committed 3 years ago

0606d7ca

feat(logic/basic): Generalize `congr_fun_heq` (#13867)

vihdzp committed 3 years ago

3e2f2145

feat(algebra/star/prod): elementwise `star` operator (#13856)

eric-wieser committed 3 years ago

785f62c6

feat(measure_theory/integral/bochner): Add a rewrite lemma saying the ennreal coercion of an integral of a nonnegative function equals the lintegral of the ennreal coercion of the function. (#13701)

kkytola committed 3 years ago

206a5f77

feat(topology/metric_space/thickened_indicator): Add definition and lemmas about thickened indicators. (#13481)

kkytola committed 3 years ago

917b5275

feat(algebra/big_operators/finprod): add lemma `finprod_eq_prod_of_mul_support_to_finset_subset'` (#13801)

ocfnash committed 3 years ago

af11e154

feat(analysis/matrix): provide a normed_algebra structure on matrices (#13518)

eric-wieser committed 3 years ago

65843cdc

feat(linear_algebra/finite_dimensional): `finite_dimensional_iff_of_rank_eq_nsmul` (#13357)

Vierkantor committed 3 years ago

90418df5

feat(ring_theory/dedekind_domain): Chinese remainder theorem for Dedekind domains (#13067)

Vierkantor committed 3 years ago

64bc02c5

chore(.github/workflows/merge_conflicts.yaml): use separate token (#13884)

kim-em committed 3 years ago

384a7a39

feat(topology/homeomorph): add `(co)map_cocompact` (#13861)

urkud committed 3 years ago

ad2e9365

feat(category_theory/limits/shapes/types): explicit isos (#13854)

kim-em committed 3 years ago

dbc03394

feat(category_theory/preadditive): End X is a division_ring or field when X is simple (#13849)

kim-em committed 3 years ago

9d3db534

chore(model_theory/basic): golf `countable_empty` (#13836)

vihdzp committed 3 years ago

e5b48f9b

fix(algebra/indicator_function): add missing decidable instances to lemma statements (#13834)

eric-wieser committed 3 years ago

4fe734da

feat(analysis/normed_space/add_torsor_bases): add lemma `smooth_barycentric_coord` (#13764)

ocfnash committed 3 years ago

cf5fa84c

feat(linear_algebra/affine_space/basis): add lemma `affine_basis.linear_combination_coord_eq_self` (#13763)

ocfnash committed 3 years ago

4113e00a

fix(src/tactic/alias): Support `alias foo ↔ ..` as documented (#13743)

nomeata committed 3 years ago

b063c286

refactor(topology/algebra/order): reorganize, simplify proofs (#13716)

fpvandoorn committed 3 years ago

3fde0827

feat(category_theory/limits): pushouts and pullbacks in the opposite category (#13495)

joelriou committed 3 years ago

52a454af

feat(group_theory/group_action/basic): A multiplicative action induces an additive action of the additive group (#13780)

tb65536 committed 3 years ago

61d5d308

refactor(linear_algebra/trace): unbundle `matrix.trace` (#13712)

eric-wieser committed 3 years ago

320df450

feat(category_theory/monoidal): adjunctions in rigid categories (#13707)

kim-em committed 3 years ago

a6275694