proposition 4.27 Inverse of a product
open in the book ·
parts/02-mathematical-methods/02-algebraic-structures.tex:677
· p. 65
Rests on
-
depends_on
definition 4.21
Group
¶
-
depends_on
definition 4.11
Inverse element
¶
-
depends_on
definition 4.9
Neutral element
¶
-
depends_on
definition 4.3
Algebraic structure
¶
- depends_on definition 4.2 Binary operation ¶
-
depends_on
definition 4.3
Algebraic structure
¶
-
depends_on
definition 4.9
Neutral element
¶
-
depends_on
definition 4.20
Monoid
¶
- depends_on definition 4.9 Neutral element ¶ ↺
-
depends_on
definition 4.18
Semigroup
¶
-
depends_on
definition 4.6
Associativity
¶
- depends_on definition 4.3 Algebraic structure ¶ ↺
-
depends_on
definition 4.4
Internal binary operation; magma
¶
- depends_on definition 4.3 Algebraic structure ¶ ↺
- depends_on definition 4.2 Binary operation ¶ ↺
-
depends_on
definition 4.6
Associativity
¶
-
depends_on
definition 4.11
Inverse element
¶
-
depends_on
proposition 4.23
Uniqueness of the inverse element
¶
- depends_on definition 4.21 Group ¶ ↺
- proves proof ch:02-algebraic-structures@proof-4 ¶
- proves proof ch:02-algebraic-structures@proof-8 ¶
Supports
-
depends_on
proposition 4.57
prop:alg-conjugacy-equiv
¶
-
depends_on
definition 4.58
Conjugacy classes
¶
-
depends_on
definition 4.59
Conjugate subgroups
¶
-
depends_on
definition 4.60
Normal subgroup
¶
- depends_on proposition 4.63 Well-definedness of the coset product ¶
- depends_on proposition 4.70 Characterization of the direct product ¶
- depends_on proposition 4.75 The two factors inside the semidirect product ¶
- depends_on proposition 4.77 When a semidirect product is direct ¶
- depends_on theorem 4.64 Quotient group ¶
- depends_on theorem 4.76 Internal characterization of the semidirect product ¶
-
depends_on
definition 4.60
Normal subgroup
¶
-
depends_on
definition 4.59
Conjugate subgroups
¶
-
depends_on
definition 4.58
Conjugacy classes
¶
- depends_on proposition 4.42 When the homomorphisms form a group ¶
Neighborhood
Every logical edge within two steps of this node.
- declared and complete
- partly declared
- a check failed
- not graded
- declared in the source
- inferred from structure
Edges
| type | direction | node | provenance | where |
|---|---|---|---|---|
depends_on |
→ | Group | declared | parts/02-mathematical-methods/02-algebraic-structures.tex:682 |
depends_on |
→ | Uniqueness of the inverse element | declared | parts/02-mathematical-methods/02-algebraic-structures.tex:682 |
depends_on |
← | prop:alg-conjugacy-equiv | declared | parts/02-mathematical-methods/02-algebraic-structures.tex:2015 |
depends_on |
← | When the homomorphisms form a group | declared | parts/02-mathematical-methods/02-algebraic-structures.tex:1436 |
proves |
← | ch:02-algebraic-structures@proof-8 | declared | parts/02-mathematical-methods/02-algebraic-structures.tex:685 |