Map

📁 Source: Mathlib/Algebra/Group/WithOne/Map.lean

Statistics

Metric	Count
Definitions map, map₂, map, map₂	4
Theorems map_bot, map_coe, map₂_bot_left, map₂_bot_right, map₂_coe_coe, map₂_coe_left, map₂_coe_right, map₂_eq_bot_iff, map_bot, map_coe, map₂_bot_left, map₂_bot_right, map₂_coe_coe, map₂_coe_left, map₂_coe_right, map₂_eq_bot_iff	16
Total	20

WithOne

Definitions

Name	Category	Theorems
map 📖	CompOp	4 math math: map_coe, map_bot, map₂_coe_right, map₂_coe_left
map₂ 📖	CompOp	6 math math: map₂_bot_left, map₂_bot_right, map₂_eq_bot_iff, map₂_coe_coe, map₂_coe_right, map₂_coe_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_bot 📖	mathematical	—	map WithOne instOne	—	—
map_coe 📖	mathematical	—	map coe	—	—
map₂_bot_left 📖	mathematical	—	map₂ WithOne instOne	—	—
map₂_bot_right 📖	mathematical	—	map₂ WithOne instOne	—	—
map₂_coe_coe 📖	mathematical	—	map₂ coe	—	—
map₂_coe_left 📖	mathematical	—	map₂ coe map	—	—
map₂_coe_right 📖	mathematical	—	map₂ coe map	—	—
map₂_eq_bot_iff 📖	mathematical	—	map₂ WithOne instOne	—	Option.map₂_eq_none_iff

WithZero

Definitions

Name	Category	Theorems
map 📖	CompOp	4 math math: map_bot, map₂_coe_left, map₂_coe_right, map_coe
map₂ 📖	CompOp	6 math math: map₂_eq_bot_iff, map₂_bot_left, map₂_coe_left, map₂_coe_right, map₂_bot_right, map₂_coe_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_bot 📖	mathematical	—	map WithZero instZero	—	—
map_coe 📖	mathematical	—	map coe	—	—
map₂_bot_left 📖	mathematical	—	map₂ WithZero instZero	—	—
map₂_bot_right 📖	mathematical	—	map₂ WithZero instZero	—	—
map₂_coe_coe 📖	mathematical	—	map₂ coe	—	—
map₂_coe_left 📖	mathematical	—	map₂ coe map	—	—
map₂_coe_right 📖	mathematical	—	map₂ coe map	—	—
map₂_eq_bot_iff 📖	mathematical	—	map₂ WithZero instZero	—	Option.map₂_eq_none_iff

---

← Back to Index