Metamath Proof Explorer

Syntax definition cufd

Description: Class of unique factorization domains.

Ref Expression
Assertion cufd 
class UFD