Commits leanprover-community/mathlib3

Merge remote-tracking branch 'origin/master' into JasonKYi/layercake

kex-y committed 3 years ago

99521aab

feat(measure_theory/function/conditional_expectation): conditional expectation with respect to the bot sigma algebra (#16342)

RemyDegenne committed 3 years ago

745e23d5

initial

kex-y committed 3 years ago

1d0c1ff7

feat(data/{seq,stream}): cons_injective2 (#15832)

vihdzp committed 3 years ago

3c006126

chore(probability/martingale): move the optional stopping theorem to its own file (#16464)

RemyDegenne committed 3 years ago

87714908

refactor(algebra/order/monoid): Remove redundant field from `ordered_cancel_comm_monoid` (#16445)

YaelDillies committed 3 years ago

d04db585

feat(topology/uniform_space/compact_separated): drop unneeded assumptions (#16457)

urkud committed 3 years ago

27917391

feat(data/fintype/basic): `fintype.to_finset_prod` (#16459)

kmill committed 3 years ago

c8c740df

feat(algebra/parity): Primes are not square (#16430)

YaelDillies committed 3 years ago

5e78882f

refactor(analysis/normed_space/spectrum): generalize Gelfand-Mazur away from `normed_division_ring` (#16448)

j-loreaux committed 3 years ago

ba6b1422

feat(probability/stopping): generalize `mem_ℒp_stopped_value` (#16369)

RemyDegenne committed 3 years ago

7fd4a0bf

feat(counterexamples/sorgenfrey_line): new file (#14820)

urkud committed 3 years ago

f7d03fec

feat(linear_algebra/linear_pmap): add_action and mul_action (#16068)

mcdoll committed 3 years ago

48e3d6a4

feat(topology/algebra/module/weak_dual): `weak_space` is functorial (#16441)

ADedecker committed 3 years ago

22a9066d

feat(analysis/inner_product_space/basic): completion of an `inner_product_space` is an `inner_product_space` (#16407)

ADedecker committed 3 years ago

c3d2b3b8

feat(analysis/{normed/group}/seminorm): Hom classes for seminorms (#16227)

YaelDillies committed 3 years ago

3a0b839b

feat(analysis/normed/group/basic): add `norm_multiset_sum_le` (#16419)

astrainfinita committed 3 years ago

75cc1ae9

feat(order/upper_lower): `Iic` is not bounded below (#16425)

YaelDillies committed 3 years ago

ba346d8b

feat(number_theory/legendre_symbol/jacobi_symbol): add new file with the definition and properties of the Jacobi symbol (#16395)

MichaelStollBayreuth committed 3 years ago

d2d66526

refactor(data/{finite,fintype}): redefine `infinite` in terms of `finite`, move to `data.finite.defs` (#16390)

urkud committed 3 years ago

662786a8

feat(combinatorics/young_diagram): add transposes, rows and columns of Young diagrams (#16120)

jakelev committed 3 years ago

e0bdbbe1

feat(ring_theory/dedekind_domain/integer_unit): define S-integers and S-units (#15646)

Multramate committed 3 years ago

00ab7761

feat(combinatorics/simple_graph/triangle/basic): add ε-triangle-free far graph predicate (#12988)

YaelDillies committed 3 years ago

cd7f0626

feat(analysis/calculus/uniform_limits_deriv): Swap limits and derivatives (#14090)

khwilson committed 3 years ago

d645d0e8

chore(algebra/big_operators/basic): golf (#16427)

astrainfinita committed 3 years ago

aff61c0f

fix(data/nat/interval): do not dedup when implementing `finset.Icc` etc (#16423)

eric-wieser committed 3 years ago

d75314b3

feat(algebra/big_operators/multiset): add `prod_map_le_prod_map` (#16418)

astrainfinita committed 3 years ago

370dabe7

fix(*): fix padding around notations (#16333)

digama0 committed 3 years ago

a0735864

feat(analysis/schwartz): Definition of the Schwartz space (#15850)

mcdoll committed 3 years ago

4c0aa6e7

feat(number_theory/modular_forms/congruence_subgroups): Add definition of congruence subgroups. (#15159)

CBirkbeck committed 3 years ago

9b6eef6e