Commit 2026-05-08 06:03 b45f853d
View on Github →chore(Mathlib/Probability/Kernel/Composition/KernelLemmas.lean): automated extraction (#39042) This PR was automatically created from PR #37851 by @gaetanserre via a review comment by @dagurtomas.
chore(Mathlib/Probability/Kernel/Composition/KernelLemmas.lean): automated extraction (#39042) This PR was automatically created from PR #37851 by @gaetanserre via a review comment by @dagurtomas.