gpt4 book ai didi

typeclass - 在精益类定义中扩展或推断(PID/UFD)

转载 作者:行者123 更新时间:2023-12-03 08:15:43 26 4
gpt4 key购买 nike

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

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

最佳答案

我的印象来自discussion on the Lean chat是因为与类型类推断相关的微妙原因,扩展类可能更好,因此可能需要重构 UFD 的定义。

关于typeclass - 在精益类定义中扩展或推断(PID/UFD),我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/60130605/

26 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com