English
For a field 𝕜 and an algebra A over 𝕜, the polynomial annIdealGenerator 𝕜 a is the monic generator of the annihilating ideal annIdeal 𝕜 a; if the ideal is zero this generator is defined as 0.
Русский
Для поля 𝕜 и алгебры A над 𝕜, полином annIdealGenerator 𝕜 a является моническим генератором аннигиляционного идеала annIdeal 𝕜 a; если идеал нулевой, генератор определяется как 0.
LaTeX
$$$\text{annIdealGenerator}_{\mathbb{k}}(a) \text{ является моническим генератором }\operatorname{annIdeal}_{\mathbb{k}}(a)\quad\text{или}\\ annIdeal_{\mathbb{k}}(a)=\{0\}.$$$
Lean4
/-- `annIdealGenerator 𝕜 a` is the monic generator of `annIdeal 𝕜 a`
if one exists, otherwise `0`.
Since `𝕜[X]` is a principal ideal domain there is a polynomial `g` such that
`span 𝕜 {g} = annIdeal a`. This picks some generator.
We prefer the monic generator of the ideal. -/
noncomputable def annIdealGenerator (a : A) : 𝕜[X] :=
let g := IsPrincipal.generator <| annIdeal 𝕜 a
g * C g.leadingCoeff⁻¹
