Theorem MvQPF.liftR_iff

Modification history

2025-04-09 21:09

Mathlib/Data/QPF/Multivariate/Basic.lean

chore(QPF/Multivariate/Basic): use strict implicit binder in `liftR_iff` (#23880) …

Modified MvQPF.liftR_iff View on Github →

2023-02-20 12:18

Mathlib/Data/QPF/Multivariate/Basic.lean

feat: Port Data.QPF.Multivariate.Basic (#2223)

Added MvQPF.liftR_iff View on Github →