subOnePowerBasis — Mathlib

English

There is an equivalence between algebra homomorphisms from L to C and primitive roots in C, parameterized by a fixed primitive root ζ.

Русский

Существует эквивалентность между алгебра-моморфизмами L→C и примитивными корнями в C, заданная фиксированным ζ.

LaTeX

$$$(L \to_{K} C) \simeq primitiveRoots(n, C)$$

Lean4

/-- The `PowerBasis` given by `η - 1`. -/
@[simps!]
noncomputable def subOnePowerBasis : PowerBasis K L :=
  by
  apply PowerBasis.ofAdjoinEqTop (((integral { n } K L).isIntegral ζ).sub isIntegral_one)
  exact PowerBasis.adjoin_eq_top_of_gen_mem_adjoin (hζ.powerBasis_gen_mem_adjoin_zeta_sub_one _)

Похожие утверждения