Const

📁 Source: Mathlib/Data/QPF/Multivariate/Constructions/Const.lean

Statistics

Metric	Count
Definitions Const, MvFunctor, get, inhabited, map, mk, mvqpf	7
Theorems get_map, get_mk, map_mk, mk_get	4
Total	11

MvQPF

Definitions

Name	Category	Theorems
Const 📖	CompOp	2 math math: Const.map_mk, Const.get_map

MvQPF.Const

Definitions

Name	Category	Theorems
MvFunctor 📖	CompOp	2 math math: map_mk, get_map
get 📖	CompOp	3 math math: mk_get, get_map, get_mk
inhabited 📖	CompOp	—
map 📖	CompOp	—
mk 📖	CompOp	—
mvqpf 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
get_map 📖	mathematical	—	get MvFunctor.map MvQPF.Const MvFunctor	—	—
get_mk 📖	mathematical	—	get	—	—
map_mk 📖	mathematical	—	MvFunctor.map MvQPF.Const MvFunctor	—	—
mk_get 📖	mathematical	—	get	—	—

---

← Back to Index