Each relation below ends at this concept.
This is an authored directed relation from the source endpoint to the target endpoint.
- Relation ID
euclidean_domain_to_pid- Relation type
- Theorem implication
theorem-implication - Direction
- source → target
- Endpoint roles
- source: Implies by theorem; target: Follows by theorem from
- Authored annotation
- is a PID
Authored explanation
The Euclidean algorithm implies every ideal is principal.
How to interpret this relation type
Record a genuine theorem implication that is not part of the target definition; these edges may point toward a weaker structure.
This is an authored directed relation from the source endpoint to the target endpoint.
- Relation ID
ufd_to_pid- Relation type
- Impose axiom
impose-axiom - Direction
- source → target
- Endpoint roles
- source: Builds toward; target: Built from
- Authored annotation
- require principal ideals
Authored explanation
Require every ideal to have one generator.
How to interpret this relation type
Keep the existing data and select the subclass satisfying an additional law, existence condition, finiteness condition, or other property.