map_of_injective — Mathlib

English

If f is an injective monoid hom, then primitiveRoot maps forward: IsPrimitiveRoot( f ζ, k ).

Русский

Если f — инъективный гомоморфизм моноидов, то примитивный корень сохраняется под отображением: IsPrimitiveRoot(f ζ, k).

LaTeX

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

Lean4

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

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