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

为什么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)

扩展积分域结构？有什么区别？旧的结构命令与此有关吗？