Hom
📁 Source: Mathlib/Algebra/Group/Commute/Hom.lean
Statistics
| Metric | Count |
|---|---|
| Definitions | 0 |
Theoremsmap, 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 | DFunLike.coe | — | AddSemiconjBy.map |
of_map 📖 | — | DFunLike.coeAddCommute | — | — | map_addeq |
AddSemiconjBy
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
map 📖 | mathematical | AddSemiconjBy | DFunLike.coe | — | map_add |
of_map 📖 | — | DFunLike.coeAddSemiconjBy | — | — | map_add |
Commute
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
map 📖 | mathematical | Commute | DFunLike.coe | — | SemiconjBy.map |
of_map 📖 | — | DFunLike.coeCommute | — | — | map_muleq |
SemiconjBy
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
map 📖 | mathematical | SemiconjBy | DFunLike.coe | — | map_mul |
of_map 📖 | — | DFunLike.coeSemiconjBy | — | — | map_mul |
(root)
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
addCommute_map_iff 📖 | mathematical | DFunLike.coe | AddCommute | — | AddCommute.of_mapAddCommute.map |
addSemiconjBy_map_iff 📖 | mathematical | DFunLike.coe | AddSemiconjBy | — | AddSemiconjBy.of_mapAddSemiconjBy.map |
commute_map_iff 📖 | mathematical | DFunLike.coe | Commute | — | Commute.of_mapCommute.map |
semiconjBy_map_iff 📖 | mathematical | DFunLike.coe | SemiconjBy | — | SemiconjBy.of_mapSemiconjBy.map |
---