leanprover-community/mathlib3

Pull Requests Commits

feat(analysis/special_functions/complex/arg): lemmas about `arg z` and `±(π / 2)` (#13821)

urkud committed 3 years ago

8a5b4a7c

chore(data/matrix/basic): add lemmas about powers of matrices (#13815)

eric-wieser committed 3 years ago

2f38ccb4

feat(ring_theory/polynomial/basic): reduce assumptions, golf (#13800)

astrainfinita committed 3 years ago

36b5341d

feat(analysis/calculus/cont_diff): cont_diff_succ_iff_fderiv_apply (#13797)

fpvandoorn committed 3 years ago

6d2788c2

feat(analysis/normed_space): lemmas about continuous bilinear maps (#13522)

fpvandoorn committed 3 years ago

234b3df2

feat(data/zmod/basic): Add `zmod.cast_sub_one` (#13889)

tb65536 committed 3 years ago

3b971a7b

chore(data/nat/totient): golf three lemmas (#13886)

stuart-presnell committed 3 years ago

78c86e1d

feat(set_theory/ordinal_basic): `o.out.α` is equivalent to the ordinals below `o` (#13876)

vihdzp committed 3 years ago

9f818ce0

feat(set_theory/game/nim): Mark many lemmas as `simp` (#13844)

vihdzp committed 3 years ago

82b9c42f

chore(order/*): Replace total partial orders by linear orders (#13839)

YaelDillies committed 3 years ago

e104992d

fix(data/complex/basic): make complex addition computable again (#13837)

eric-wieser committed 3 years ago

f6cb9be2

feat(set_theory/game/basic): Add `le_rfl` on games (#13814)

vihdzp committed 3 years ago

b07c0f70

feat(data/real/nnreal): add `nnreal.forall` and `nnreal.exists` (#13774)

urkud committed 3 years ago

72816f95

feat(order/conditionally_complete_lattice): Simp theorems (#13756)

vihdzp committed 3 years ago

7931ba44

chore(.github/workflows): use separate secret token for dependent issues (#13902)

kim-em committed 3 years ago

65cad418

ci(elan): update dead repository URLs (#13906)

eric-wieser committed 3 years ago

1c392671

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

Newer Older