pow_mem_of_index_ne_zero_of_dvd — Mathlib

English

If H.index ≠ 0 and n is divisible by every m with 0 < m ≤ H.index, then a^n ∈ H for all a ∈ G.

Русский

Если H.index ≠ 0 и n делится на каждое m, 0 < m ≤ H.index, то для всех a ∈ G выполняется a^n ∈ H.

LaTeX

$$H.index \neq 0 \Rightarrow (\forall n, (\forall m, 0 < m \rightarrow m \le H.index \rightarrow m \mid n) \Rightarrow a^n \in H)$$

Lean4

@[to_additive]
theorem pow_mem_of_index_ne_zero_of_dvd (h : H.index ≠ 0) (a : G) {n : ℕ} (hn : ∀ m, 0 < m → m ≤ H.index → m ∣ n) :
    a ^ n ∈ H := by
  rcases exists_pow_mem_of_index_ne_zero h a with ⟨m, hlt, hle, he⟩
  rcases hn m hlt hle with ⟨k, rfl⟩
  rw [pow_mul]
  exact pow_mem he _

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