Graded

📁 Source: Mathlib/Data/FunLike/Graded.lean

Statistics

Metric	Count
Definitions equiv, subtypeMap, GradedEquivLike, GradedFunLike	4
Theorems equiv_apply, equiv_symm_apply_coe, map_mem, map_mem_iff, map_mem_of_mem, mem_of_map_mem, map_mem_iff, toGradedFunLike, map_mem	9
Total	13

Graded

Definitions

Name	Category	Theorems
equiv 📖	CompOp	2 math math: equiv_apply, equiv_symm_apply_coe
subtypeMap 📖	CompOp	1 math math: equiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv_apply 📖	mathematical	—	DFunLike.coe Equiv SetLike.instMembership EquivLike.toFunLike Equiv.instEquivLike equiv subtypeMap GradedEquivLike.toGradedFunLike	—	—
equiv_symm_apply_coe 📖	mathematical	—	SetLike.instMembership DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equiv EquivLike.inv	—	—
map_mem 📖	mathematical	SetLike.instMembership	SetLike.instMembership DFunLike.coe	—	GradedFunLike.map_mem
map_mem_iff 📖	mathematical	—	SetLike.instMembership DFunLike.coe EquivLike.toFunLike	—	GradedEquivLike.map_mem_iff
map_mem_of_mem 📖	mathematical	SetLike.instMembership	SetLike.instMembership DFunLike.coe EquivLike.toFunLike	—	map_mem_iff
mem_of_map_mem 📖	mathematical	SetLike.instMembership DFunLike.coe EquivLike.toFunLike	SetLike.instMembership	—	map_mem_iff

GradedEquivLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_mem_iff 📖	mathematical	—	SetLike.instMembership DFunLike.coe EquivLike.toFunLike	—	—
toGradedFunLike 📖	mathematical	—	GradedFunLike EquivLike.toFunLike	—	map_mem_iff

GradedFunLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_mem 📖	mathematical	SetLike.instMembership	SetLike.instMembership DFunLike.coe	—	—

(root)

Definitions

Name	Category	Theorems
GradedEquivLike 📖	CompData	—
GradedFunLike 📖	CompData	3 math math: GradedRingHom.instGradedFunLike, GradedAlgHom.instGradedFunLikeSubmodule, GradedEquivLike.toGradedFunLike

---

← Back to Index