Comp

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

Statistics

Metric	Count
Definitions get, inst, instInhabited, instMvFunctor, map, map', mk	7
Theorems get_map, get_mk, map_mk, mk_get	4
Total	11

MvQPF.Comp

Definitions

Name	Category	Theorems
get 📖	CompOp	3 math math: get_mk, get_map, mk_get
inst 📖	CompOp	—
instInhabited 📖	CompOp	—
instMvFunctor 📖	CompOp	2 math math: get_map, map_mk
map 📖	CompOp	—
map' 📖	CompOp	—
mk 📖	CompOp	—

Theorems

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

---

← Back to Index