mathlib

e5a4cda3 - add kernel corresponding to condexp