Vanishing cross terms over subfields #
If x², a, and b lie in a subfield but x does not, squaring a + b * x can land in
that subfield only when a * b = 0, provided the ambient field has characteristic different
from two.
This criterion is used in square-class descent through quadratic extensions.
theorem
TauCeti.mul_eq_zero_of_add_mul_sq_mem
{L : Type u_1}
[Field L]
{S : Type u_2}
[SetLike S L]
[SubfieldClass S L]
{F : S}
{x : L}
(hx2 : x ^ 2 ∈ F)
(hxF : x ∉ F)
[NeZero 2]
{a b : L}
(ha : a ∈ F)
(hb : b ∈ F)
(hab_mem : (a + b * x) ^ 2 ∈ F)
:
Vanishing cross term in a quadratic step. If x² ∈ F but x ∉ F, then a square
(a + b * x) ^ 2 of a normal-form element that lands back in F has no cross term: a * b = 0.
This is where characteristic not two enters, through 2 ≠ 0 in L. It holds for an arbitrary
subfield F of L; no ambient base field or algebra tower is needed.