exists_pow_mem_of_relIndex_ne_zero

English

If H.relIndex K ≠ 0 and a ∈ K, there exists n > 0 with n ≤ H.relIndex K and a^n ∈ H ∩ K.

Русский

Если H.relIndex K ≠ 0 и a ∈ K, найдётся n > 0 такое, что n ≤ H.relIndex K и a^n ∈ H ∩ K.

LaTeX

$$H.relIndex K \neq 0 \land a \in K \Rightarrow \exists n > 0, n \le H.relIndex K \land a^n \in H \cap K$$

Lean4

@[to_additive]
theorem exists_pow_mem_of_relIndex_ne_zero (h : H.relIndex K ≠ 0) {a : G} (ha : a ∈ K) :
    ∃ n, 0 < n ∧ n ≤ H.relIndex K ∧ a ^ n ∈ H ⊓ K :=
  by
  rcases exists_pow_mem_of_index_ne_zero h ⟨a, ha⟩ with ⟨n, hlt, hle, he⟩
  refine ⟨n, hlt, hle, ?_⟩
  simpa [pow_mem ha, mem_subgroupOf] using he

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