leanprover-community/mathlib3

Pull Requests Commits

vihdzp committed 3 years ago

7a2e7b3d

doc(analysis/matrix): fix broken LaTeX (#13910)

eric-wieser committed 3 years ago

40b59523

feat(linear_algebra/matrix/trace): add `trace_conj_transpose` (#13888)

eric-wieser committed 3 years ago

1c4d2b7c

feat(order/omega_complete_partial_order): make `continuous_hom.prod.apply` continuous (#13833)

nomeata committed 3 years ago

0f8d7a99

feat(topology/algebra/module/basic): A continuous linear functional is open (#13829)

YaelDillies committed 3 years ago

475a5334

move(data/pi/*): Group `pi` files (#13826)

YaelDillies committed 3 years ago

4cea0a8f

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

Older