Commits leanprover-community/mathlib

feat(set_theory/continuum): define `cardinal.continuum := 2 ^ ω` (#9354)

urkud committed 4 years ago

e18b9cac

chore(order/*): replace `mono_incr` and `mono_decr` in lemma names wih `monotone` and `antitone` (#9428)

eric-wieser committed 4 years ago

15f15a6e

fix(algebra/opposites): add a missing `comm_semiring` instance (#9425)

eric-wieser committed 4 years ago

2d5fd655

feat(data/set/intervals): add `order_iso.image_Ixx` lemmas (#9404)

urkud committed 4 years ago

84bbb00f

refactor(algebra/order/ring,data/complex): redefine `ordered_comm_ring` and complex order (#9420)

urkud committed 4 years ago

4a02fd3b

feat(data/list/basic): lemmas about tail (#9259)

kim-em committed 4 years ago

06610c70

feat(linear_algebra/matrix/fpow): integer powers of matrices (#8683)

pechersky committed 4 years ago

c0dbe14d

chore(analysis/special_functions): add some `@[simp]` attrs (#9423)

urkud committed 4 years ago

01adfd65

doc(*): remove docstrings from copyright headers (#9411)

YaelDillies committed 4 years ago

61086166

doc(order/*): use "monotone" / "antitone" in place of "monotonically increasing" / "monotonically decreasing" (#9408)

YaelDillies committed 4 years ago

36c09f7b

chore(measure_theory/integral/interval_integral): change of variables for normed-space target (#9350)

hrmacbeth committed 4 years ago

22f24091

feat(analysis/normed_space/is_bounded_bilinear_map): direct proof of continuity (#9390)

hrmacbeth committed 4 years ago

1db626ee

feat(measure_theory/integral/interval_integral): one more FTC-2 (#9409)

urkud committed 4 years ago

4b5bf56b

feat(analysis/special_functions/complex/log): `exp ⁻¹' s` is countable (#9410)

urkud committed 4 years ago

8c5d93b0

feat(analysis/special_functions): limits of `arg` and `log` at a real negative (#9406)

urkud committed 4 years ago

b21bc971

feat(*): Clean up some misstated lemmas about algebra (#9417)

alexjbest committed 4 years ago

82795105

feat(data/polynomial/algebra_map): aeval_tower (#9250)

ChrisHughes24 committed 4 years ago

0d37fd67

chore(analysis/special_functions/exp_log): add some missing dot notation lemmas (#9405)

urkud committed 4 years ago

f181d81f

refactor(analysis/convex/function): generalize lemmas about convexity/concavity of functions, prove concave Jensen (#9356)

YaelDillies committed 4 years ago

9175158f

feat(analysis/calculus/fderiv): generalize `const_smul` lemmas (#9399)

urkud committed 4 years ago

5dfb76f5

feat(data/nat/choose/cast): Cast of binomial coefficients equals a Pochhammer polynomial (#9394)

YaelDillies committed 4 years ago

954896a1

refactor(data/fin): drop `fin.cast_add_right` (#9371)

urkud committed 4 years ago

9a30f8cf

chore(order/*): rename `strict_mono_{incr,decr}_on` to `strict_{mono,anti}_on` (#9401)

eric-wieser committed 4 years ago

850784cf

chore(order): globally replace "antimono" with "antitone" (#9400)

eric-wieser committed 4 years ago

14727997

docs(docker): adjust readme to reflect that the PR was merged (#9303)

eric-wieser committed 4 years ago

d1c68ef7

chore(measure_theory/decomposition/lebesgue): rename `radon_nikodym_deriv` to `rn_deriv` (#9386)

kex-y committed 4 years ago

cafd6fbc

refactor(analysis/special_functions/trigonometric): split file (#9340)

kim-em committed 4 years ago

a4b92a3f

refactor(measure_theory/measure/hausdorff): move `dimH` to a new file, redefine (#9391)

urkud committed 4 years ago

62abfe52

feat(algebra/pointwise): add smul_set_inter (#9374)

alexjbest committed 4 years ago

432271f9

feat(topology/sheaves/stalks): Generalize from Type to algebraic categories (#9357)

justus-springer committed 4 years ago

996783ce