Each relation below ends at this concept.
This is an authored directed relation from the source endpoint to the target endpoint.
- Relation ID
comm_ring_to_integral_domain- Relation type
- Impose axiom
impose-axiom - Direction
- source → target
- Endpoint roles
- source: Builds toward; target: Built from
- Authored annotation
- exclude zero divisors
Authored explanation
Require 1=0 and require a product to vanish only when one factor vanishes.
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.
This is an authored directed relation from the source endpoint to the target endpoint.
- Relation ID
integers_to_integral_domain- Relation type
- Induced / forgotten
induced-forgotten - Direction
- source → target
- Endpoint roles
- source: Yields by induction / forgetting; target: Obtained by induction / forgetting from
- Authored annotation
- forget order
Authored explanation
Forgetting the order leaves an integral domain.
How to interpret this relation type
Pass canonically from a stronger object to structure it determines, or forget part of the data while retaining a valid weaker structure. The carrier may change under a canonical induced construction.
Relation sources
- nLab — integer — integer · mathematical reference · source ID
nlab-integer