在精益类定义中扩展或推断（PID / UFD）

Question

为什么 mathlib 对 UFD 的定义是这样的：

class unique_factorization_domain (? : Type*) [integral_domain ?] :=
(factors : ? ? multiset ?)
(factors_prod : ?{a : ?}, a ? 0 ? (factors a).prod ~? a)
(prime_factors : ?{a : ?}, a ? 0 ? ?x?factors a, prime x)

（要求通过类型类推断来推断整数域结构）但它对 PID 的定义是这样的：

class principal_ideal_domain (? : Type*) extends integral_domain ? :=
(principal : ? (S : ideal ?), S.is_principal)

扩展整体域结构？有什么不同？旧的结构命令与它有关吗？

Answer 1

我对精益聊天讨论的印象是，由于与类型类推断相关的微妙原因，扩展类可能会更好，因此也许 UFD 的定义需要重构。