rootsOfUnityEquivOfPrimitiveRoots_symm_apply

English

A symmetry between roots of unity and primitive roots preserves the pairing with integers.

Русский

Симметрия между корнями единицы и примитивными корнями сохраняет соответствие с целыми числами.

LaTeX

$$rootsOfUnityEquivOfPrimitiveRoots(hf,hζ).symm η = ξ$$

Lean4

theorem _root_.rootsOfUnityEquivOfPrimitiveRoots_symm_apply {S F} [CommRing S] [IsDomain S] [FunLike F R S]
    [MonoidHomClass F R S] {n : ℕ} [NeZero n] {f : F} (hf : Function.Injective f) (hζ : (primitiveRoots n R).Nonempty)
    (η) : f ((rootsOfUnityEquivOfPrimitiveRoots hf hζ).symm η : Rˣ) = (η : Sˣ) :=
  by
  obtain ⟨ε, rfl⟩ := (rootsOfUnityEquivOfPrimitiveRoots hf hζ).surjective η
  rw [MulEquiv.symm_apply_apply, val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe]

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