注册
登录
精益
在精益类定义中扩展或推断（PID / UFD）
返回
在精益类定义中扩展或推断（PID / UFD）
作者:
狗头军师
发布时间:
2025-02-10 05:49:02 (6小时前)
<p>为什么mathlib对UFD的定义是这样的：</p> <pre><code>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) </code></pre><p>（要求通过类型类推断来推断积分域结构），但它对PID的定义是：</p> <pre><code>class principal_ideal_domain (α : Type*) extends integral_domain α := (principal : ∀ (S : ideal α), S.is_principal) </code></pre><p>扩展积分域结构？有什么区别？旧的结构命令与此有关吗？</p>
收藏
举报
2 条回复
1#
回复此人
v-star*위위
|
2020-08-19 15-54
从关于精益聊天的讨论中，我的印象是，由于与类型类推断有关的细微原因，扩展类可能更好，因此，也许需要重构UFD的定义。
编辑
登录
后才能参与评论
