Hom

📁 Source: Mathlib/Algebra/Group/Commute/Hom.lean

Statistics

Metric	Count
Definitions	0
Theorems map, of_map, map, of_map, map, of_map, map, of_map, addCommute_map_iff, addSemiconjBy_map_iff, commute_map_iff, semiconjBy_map_iff	12
Total	12

AddCommute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map 📖	mathematical	AddCommute	AddCommute DFunLike.coe	—	AddSemiconjBy.map
of_map 📖	mathematical	DFunLike.coe AddCommute	AddCommute	—	map_add eq

AddSemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map 📖	mathematical	AddSemiconjBy	AddSemiconjBy DFunLike.coe	—	map_add
of_map 📖	mathematical	DFunLike.coe AddSemiconjBy	AddSemiconjBy	—	map_add

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map 📖	mathematical	Commute	Commute DFunLike.coe	—	SemiconjBy.map
of_map 📖	mathematical	DFunLike.coe Commute	Commute	—	map_mul eq

SemiconjBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map 📖	mathematical	SemiconjBy	SemiconjBy DFunLike.coe	—	map_mul
of_map 📖	mathematical	DFunLike.coe SemiconjBy	SemiconjBy	—	map_mul

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addCommute_map_iff 📖	mathematical	DFunLike.coe	AddCommute DFunLike.coe	—	AddCommute.of_map AddCommute.map
addSemiconjBy_map_iff 📖	mathematical	DFunLike.coe	AddSemiconjBy DFunLike.coe	—	AddSemiconjBy.of_map AddSemiconjBy.map
commute_map_iff 📖	mathematical	DFunLike.coe	Commute DFunLike.coe	—	Commute.of_map Commute.map
semiconjBy_map_iff 📖	mathematical	DFunLike.coe	SemiconjBy DFunLike.coe	—	SemiconjBy.of_map SemiconjBy.map

---

← Back to Index