English
If there is an equivalence e: M ≃ M' along with a relation between r and s via h, then IsSMulRegular M r holds iff IsSMulRegular M' s holds.
Русский
Если существует эквивелентность e: M ≃ M' и связь между r и s через h, тогда IsSMulRegular M r эквивалентно IsSMulRegular M' s.
LaTeX
$$$IsSMulRegular M r \iff IsSMulRegular M' s$ under the hypothesis h: \forall x, e(r\cdot x) = s\cdot e x$$
Lean4
/-- An element `a` is `M`-regular if and only if a positive power of `a` is `M`-regular. -/
theorem pow_iff {n : ℕ} (n0 : 0 < n) : IsSMulRegular M (a ^ n) ↔ IsSMulRegular M a :=
by
refine ⟨?_, pow n⟩
rw [← Nat.succ_pred_eq_of_pos n0, pow_succ, ← smul_eq_mul]
exact of_smul _
