English
Noncomputable definition of an isomorphism between adjoin ℤ of {ζ} and 𝓞 K, as in IsPrimitiveRoot.adjoinEquivRingOfIntegers'.
Русский
Не вычисляемое определение изоморфизма между adjoin ℤ от {ζ} и 𝓞 K согласно IsPrimitiveRoot.adjoinEquivRingOfIntegers'.
LaTeX
$$$$ \text{IsPrimitiveRoot.adjoinEquivRingOfIntegers'}(\zeta) : \text{adjoin}_{\mathbb{Z}}({\zeta}) \cong 𝓞_K $$$$
Lean4
/-- The integral `PowerBasis` of `𝓞 K` given by a primitive root of unity, where `K` is a `p`-th
cyclotomic extension of `ℚ`. -/
noncomputable def integralPowerBasis' [hcycl : IsCyclotomicExtension { p } ℚ K] (hζ : IsPrimitiveRoot ζ p) :
PowerBasis ℤ (𝓞 K) :=
have : IsCyclotomicExtension {p ^ 1} ℚ K := by convert hcycl; rw [pow_one]
integralPowerBasis (p := p) (k := 1) (ζ := ζ) (by rwa [pow_one])
