Rescaling generators by the base field #
Multiplying each generator of an intermediate field by a nonzero scalar from the base field does
not change the field it generates: the base scalars and their inverses are already there. This is
the field-theoretic content of "generators matter only up to their square class" arguments, where
a generator √(a c²) is replaced by √a = c⁻¹ · √(a c²).
Main results #
TauCeti.IntermediateField.adjoin_range_algebraMap_mul: for nonzerou : ι → K,K(u i · x i : i) = K(x i : i).
theorem
TauCeti.IntermediateField.adjoin_range_algebraMap_mul
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
{ι : Type u_3}
{u : ι → K}
(hu : ∀ (i : ι), u i ≠ 0)
(x : ι → L)
:
IntermediateField.adjoin K (Set.range fun (i : ι) => (algebraMap K L) (u i) * x i) = IntermediateField.adjoin K (Set.range x)
Rescaling generators by nonzero base scalars. If every u i is a nonzero element of the
base field K, then the family (u i) · x i generates the same intermediate field of L / K as
the family x.