Commit 2024-08-11 23:33 c13b15d0

feat(GroupTheory/Index): exists_pow_mem_of_index_ne_zero (#15701) Add the lemma

@[to_additive]
lemma exists_pow_mem_of_index_ne_zero (h : H.index ≠ 0) (a : G) :
    ∃ n, 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H := by

and three similar lemmas. These are essentially more general versions of sq_mem_of_index_two for arbitrary finite index. From AperiodicMonotilesLean.