Commit 2023-02-21 08:42 359b44ca

View on Github →

feat: Port Data.QPF.Multivariate.Constructions.Prj (#2226)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/QPF/Multivariate/Constructions/Prj.lean

added def MvQPF.Prj.P

added def MvQPF.Prj.abs

added def MvQPF.Prj.map

added def MvQPF.Prj.repr

added def MvQPF.Prj