论文标题
ACL2中的二次扩展
Quadratic Extensions in ACL2
论文作者
论文摘要
给定次k，二次扩展场L是k的扩展，可以通过添加K中的二次多项式的根来生成K。此外，我们表明，仅仅是因为二次扩展字段的结构，例如2的Cube根和PI/9的余弦不属于K_i。特别是，这用于表明2和pi/9的余弦的立方根不是理性的。
Given a field K, a quadratic extension field L is an extension of K that can be generated from K by adding a root of a quadratic polynomial with coefficients in K. This paper shows how ACL2(r) can be used to reason about chains of quadratic extension fields Q = K_0, K_1, K_2, ..., where each K_i+1 is a quadratic extension field of K_i. Moreover, we show that some specific numbers, such as the cube root of 2 and the cosine of pi/9, cannot belong to any of the K_i, simply because of the structure of quadratic extension fields. In particular, this is used to show that the cube root of 2 and cosine of pi/9 are not rational.
