Commit 2025-04-09 21:09 012336b0
View on Github →chore(QPF/Multivariate/Basic): use strict implicit binder in liftR_iff (#23880)
This matches mathlib3 and fixes a comment in the file (which was made before Lean 4 got strict implicit binders).
The analogous lemma liftP_iff uses a strict implicit binder.
The stray comment was pointed out by the linter in #22760.