Commit 2023-02-20 19:07 ed2a34e4

View on Github →

feat: Port Data.QPF.Multivariate.Constructions.Const (#2224)

Estimated changes

Modified Mathlib.lean

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

added theorem MvQPF.Const.get_map

added theorem MvQPF.Const.map_mk

added def MvQPF.Const