pow_mem_of_relIndex_ne_zero_of_dvd

English

If H.relIndex K ≠ 0 and a ∈ K, then for any n with divisibility by all m ≤ H.relIndex K, a^n ∈ H ∩ K.

Русский

Если H.relIndex K ≠ 0 и a ∈ K, то при любом n, делящем все m ≤ H.relIndex K, выполняется a^n ∈ H ∩ K.

LaTeX

$$H.relIndex K \neq 0 \land a ∈ K \Rightarrow \forall n, (\forall m, 0 < m \rightarrow m \le H.relIndex K \rightarrow m \mid n) \Rightarrow a^n \in H \cap K$$

Lean4

@[to_additive]
theorem pow_mem_of_relIndex_ne_zero_of_dvd (h : H.relIndex K ≠ 0) {a : G} (ha : a ∈ K) {n : ℕ}
    (hn : ∀ m, 0 < m → m ≤ H.relIndex K → m ∣ n) : a ^ n ∈ H ⊓ K :=
  by
  convert pow_mem_of_index_ne_zero_of_dvd h ⟨a, ha⟩ hn
  simp [pow_mem ha, mem_subgroupOf]

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