of_map_of_injective — Mathlib

English

If IsPrimitiveRoot(f ζ, k) and f is injective, then IsPrimitiveRoot ζ k.

Русский

Если IsPrimitiveRoot(f ζ, k) и f инъективен, тогда IsPrimitiveRoot ζ k.

LaTeX

$$$$ IsPrimitiveRoot( f\zeta, k) \land \text{Injective}(f) \Rightarrow IsPrimitiveRoot(\zeta, k). $$$$

Lean4

theorem of_map_of_injective [MonoidHomClass F M N] (h : IsPrimitiveRoot (f ζ) k) (hf : Injective f) :
    IsPrimitiveRoot ζ k where
  pow_eq_one := by apply_fun f; rw [map_pow, map_one, h.pow_eq_one]
  dvd_of_pow_eq_one := by
    rw [h.eq_orderOf]
    intro l hl
    apply_fun f at hl
    rw [map_pow, map_one] at hl
    exact orderOf_dvd_of_pow_eq_one hl

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