Commits leanprover-community/mathlib3

chore(measure_theory/function/conditional_expectation): split `measure_theory.function.conditional_expectation.basic` (#19177)

RemyDegenne committed 2 years ago

d8bbb04e

chore(*): add mathlib4 synchronization comments (#19176)

leanprover-community-bot committed 2 years ago

087c325a

refactor(data/nat/nth): redefine, review API (#18760)

urkud committed 2 years ago

7fdd4f37

feat(measure_theory/integral/set_integral): First moment method (#18731)

YaelDillies committed 2 years ago

ccdbfb6e

chore(*): add mathlib4 synchronization comments (#19174)

leanprover-community-bot committed 2 years ago

660b3a2d

chore(number_theory/legendre_symbol/gauss_eisenstein_lemmas): move zmod.wilsons_lemma (#19172)

Ruben-VandeVelde committed 2 years ago

c471da71

feat(linear_algebra/free_module/ideal_quotient): prove dimension of quotient by ideal equals degree of norm of generator (#19121)

Multramate committed 2 years ago

90b0d53e

feat(data/polynomial/div): add X_sub_C_dvd_sub_C_eval (#19120)

Multramate committed 2 years ago

e1e7190e

chore(*): add mathlib4 synchronization comments (#19171)

leanprover-community-bot committed 2 years ago

fd4551cf

feat(algebra/module/zlattice): prove some results about Z-lattices (#18266)

xroblot committed 2 years ago

a3e83f0f

feat(linear_algebra/matrix/nonsingular_inverse): 2×2 block triangular matrices are invertible iff their diagonal is (#18849)

eric-wieser committed 2 years ago

96aa788f

feat(probability/martingale): optional sampling theorem (#14065)

RemyDegenne committed 2 years ago

ba074af8

chore(*/centralizer): add forgotten `to_additive`s (#19168)

ericrbg committed 2 years ago

cc67cd75

chore(modular_forms/basic): fix typo in docs (#19166)

ericrbg committed 2 years ago

59150e4a

chore(*): add mathlib4 synchronization comments (#19167)

leanprover-community-bot committed 2 years ago

6b31d1ee

feat(analysis/convex/cone/proper): define proper cone (#18913)

apurvnakade committed 2 years ago

74f1d619

chore(*): add mathlib4 synchronization comments (#19165)

leanprover-community-bot committed 2 years ago

7e5137f5

feat(ring_theory/subring): centralizer as a subring (#18861)

ericrbg committed 2 years ago

b915e939

feat(algebra/star/basic): refactor `star_ordered_ring` to include `add_submonoid.closure` (#18854)

j-loreaux committed 2 years ago

31c24aa7

feat(geometry/manifold): lemmas from the sphere eversion project (#18877)

fpvandoorn committed 2 years ago

e354e865

chore(probability/kernel/composition): redefine kernel.comp using measure.bind, remove kernel.map_measure (#19160)

RemyDegenne committed 2 years ago

3b92d54a

refactor(geometry/manifold/cont_mdiff_map): refactor to reduce imports (#19164)

kim-em committed 2 years ago

0dc40792

feat (number_theory/zeta_function): func eqn + link to Bernoulli nos (#19158)

loefflerd committed 2 years ago

81843c08

chore(linear_algebra/eigenspace): split file (#19163)

kim-em committed 2 years ago

6b016921

chore(*): add mathlib4 synchronization comments (#19162)

leanprover-community-bot committed 2 years ago

c2092722

chore(algebra/algebra/spectrum): split file (#19161)

j-loreaux committed 2 years ago

58a27226

chore(*): add mathlib4 synchronization comments (#19159)

leanprover-community-bot committed 2 years ago

36938f77

feat (special_functions/gamma): doubling formula (#19136)

loefflerd committed 2 years ago

a3209ddf

chore(*): add mathlib4 synchronization comments (#19157)

leanprover-community-bot committed 2 years ago

575b4ea3

feat(topology/homotopy/homotopy_group): `group` and `comm_group` instances for `π_n` (#15681)

ralvrz committed 2 years ago

4c3e1721