map_iff_of_injective — Mathlib

English

If f is injective, IsPrimitiveRoot( f ζ, k ) is equivalent to IsPrimitiveRoot( ζ, k ).

Русский

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

LaTeX

$$$$\text{IsPrimitiveRoot}(f\zeta,k) \iff IsPrimitiveRoot(\zeta,k).$$$$

Lean4

theorem map_iff_of_injective [MonoidHomClass F M N] (hf : Injective f) :
    IsPrimitiveRoot (f ζ) k ↔ IsPrimitiveRoot ζ k :=
  ⟨fun h => h.of_map_of_injective hf, fun h => h.map_of_injective hf⟩

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