leanprover-community/mathlib3

Pull Requests Commits
feat(analysis/mellin_transform): Mellin transforms (#18822)
loefflerd committed 2 years ago
9e6d4aec
chore(algebra/order/group/defs): remove some instances that cause timeouts with etaExperiment (#18985)
kim-em committed 2 years ago
b599f4e4
feat(topology/sets/compacts): add `positive_compacts.map` (#18872)
eric-wieser committed 2 years ago
8c1b484d
chore(probability/independence): create independence folder, split old file into two parts (#18987)
RemyDegenne committed 2 years ago
2f834701
chore(*): add mathlib4 synchronization comments (#18984)
github-actions[bot] committed 2 years ago
781cb2ee
feat(analysis/normed/order/lattice): add has_solid_norm (#18554)
xroblot committed 2 years ago
5dc275ec
chore(topology/instances/ennreal): missing smul lemmas (#18980)
eric-wieser committed 2 years ago
ec4b2eeb
feat(data/finset/lattice): Distributivity lemmas (#18611)
YaelDillies committed 2 years ago
2d44d682
feat(algebra/order/to_interval_mod): add circular_order instance for add_circle (#17743)
eric-wieser committed 2 years ago
213b0cff
feat(probability/kernel/measurable_integral): the integral against a kernel is strongly measurable (#18974)
RemyDegenne committed 2 years ago
28b2a92f
isolate last sorry
RemyDegenne committed 2 years ago
b602ccde
chore(*): add mathlib4 synchronization comments (#18977)
github-actions[bot] committed 2 years ago
a2706b55
feat(number_theory/diophantine_approximation): add Legendre's thm on rat'l approximations (#18460)
MichaelStollBayreuth committed 2 years ago
e25a3174
refactor(algebra): Redefine `a ≡ b [PMOD p]` (#18958)
YaelDillies committed 2 years ago
a07d7509
feat(number_theory/pell): add def and properties of fundamental solutions (#18901)
MichaelStollBayreuth committed 2 years ago
0b20dffb
chore(algebra/order/absolute_value): remove unneeded imports (#18978)
kim-em committed 2 years ago
0013240b
add ae_strongly_measurable.integral_condexp_kernel
RemyDegenne committed 2 years ago
c5fa9699
small progress
RemyDegenne committed 2 years ago
271ae4e5
minor
RemyDegenne committed 2 years ago
629f9125
fix
RemyDegenne committed 2 years ago
8c81f640
add ae_strongly_measurable_integral_cond_kernel
RemyDegenne committed 2 years ago
5c397bb2
some work
RemyDegenne committed 2 years ago
080b0b5f
add condexp kernel
RemyDegenne committed 2 years ago
1267f7c4
Merge remote-tracking branch 'origin/RD_disintegration' into RD_condexp_kernel
RemyDegenne committed 2 years ago
685411eb
Merge remote-tracking branch 'origin/RD_integral_kernel' into RD_condexp_kernel
RemyDegenne committed 2 years ago
81a203ae
chore(representation_theory/group_cohomology): use `fin.cast_succ` instead of coe (#18950)
eric-wieser committed 2 years ago
cc5dd624
clean, docstrings, etc
RemyDegenne committed 2 years ago
eb6b6136
add integrable_cond_cdf
RemyDegenne committed 2 years ago
b5ce4761
add integral_cond_cdf
RemyDegenne committed 2 years ago
5b7c7ca0
fix
RemyDegenne committed 2 years ago
fa7c1b36
Terms Of Use Privacy Policy Refund Policy Impressum