Conjugate
📁 Source: Mathlib/Logic/Function/Conjugate.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsSemiconj₂ | 1 |
Theoremscomp_left, comp_right, id_left, id_right, option_map, refl, semiconj, commute, comp_eq, comp_left, comp_right, eq, id_left, id_right, inverse_left, inverses_right, option_map, trans, comp, comp_eq, eq, id_left, isAssociative_left, isAssociative_right, isIdempotent_left, isIdempotent_right, semiconj_iff_comp_eq | 27 |
| Total | 28 |
Function
Definitions
| Name | Category | Theorems |
|---|---|---|
Semiconj₂ 📖 | MathDef |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
semiconj_iff_comp_eq 📖 | mathematical | — | Semiconj | — | — |
Function.Commute
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
comp_left 📖 | — | Function.Commute | — | — | Function.Semiconj.comp_left |
comp_right 📖 | — | Function.Commute | — | — | Function.Semiconj.comp_right |
id_left 📖 | mathematical | — | Function.Commute | — | Function.Semiconj.id_left |
id_right 📖 | mathematical | — | Function.Commute | — | Function.Semiconj.id_right |
option_map 📖 | — | Function.Commute | — | — | Function.Semiconj.option_map |
refl 📖 | mathematical | — | Function.Commute | — | — |
semiconj 📖 | mathematical | Function.Commute | Function.Semiconj | — | — |
Function.Semiconj
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
commute 📖 | mathematical | Function.Semiconj | Function.Commute | — | — |
comp_eq 📖 | — | Function.Semiconj | — | — | Function.semiconj_iff_comp_eq |
comp_left 📖 | — | Function.Semiconj | — | — | trans |
comp_right 📖 | — | Function.Semiconj | — | — | eq |
eq 📖 | — | Function.Semiconj | — | — | — |
id_left 📖 | mathematical | — | Function.Semiconj | — | — |
id_right 📖 | mathematical | — | Function.Semiconj | — | — |
inverse_left 📖 | — | Function.Semiconj | — | — | — |
inverses_right 📖 | — | Function.Semiconj | — | — | eq |
option_map 📖 | — | Function.Semiconj | — | — | — |
trans 📖 | — | Function.Semiconj | — | — | eq |
Function.Semiconj₂
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
comp 📖 | — | Function.Semiconj₂ | — | — | eq |
comp_eq 📖 | mathematical | Function.Semiconj₂ | Function.bicomprFunction.bicompl | — | — |
eq 📖 | — | Function.Semiconj₂ | — | — | — |
id_left 📖 | mathematical | — | Function.Semiconj₂ | — | — |
isAssociative_left 📖 | — | Function.Semiconj₂ | — | — | eq |
isAssociative_right 📖 | — | Function.Semiconj₂ | — | — | Function.Surjective.forall₃eq |
isIdempotent_left 📖 | — | Function.Semiconj₂ | — | — | eq |
isIdempotent_right 📖 | — | Function.Semiconj₂ | — | — | Function.Surjective.foralleq |
---