[Merged by Bors] - chore: drop completeness from the definition of conditional expectation#39862

sgouezel wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

sgouezel:SG_noCompleteCondexpsgouezel/mathlib4:SG_noCompleteCondexpCopy head branch name to clipboard