coe_submonoidClass_iff — Mathlib

English

IsPrimitiveRoot is preserved when passing to a submonoid class and back.

Русский

Свойство примитивного корня сохраняется при переходе к подмоноиду и обратно.

LaTeX

$$$IsPrimitiveRoot(\zeta : M,k) \iff IsPrimitiveRoot(\zeta,k)$$$

Lean4

@[simp]
theorem coe_submonoidClass_iff {M B : Type*} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] {N : B} {ζ : N} :
    IsPrimitiveRoot (ζ : M) k ↔ IsPrimitiveRoot ζ k :=
  by
  simp_rw [iff_def]
  norm_cast

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