pow_right — Mathlib

English

If a semiconjugates x to y in a monoid, then for all integers m, a semiconjugates x^{m} to y^{m} (in the unit context as well).

Русский

Если a полусопрягает x к y в моноиде, то для любого целого m выполняется, что a полусопрягает x^{m} к y^{m} (в контексте юнитов аналогично).

LaTeX

$$$$\forall m\in \mathbb{Z}:\ SemiconjBy\ a\ (x^{m})\ (y^{m}).$$$$

Lean4

@[to_additive (attr := simp)]
theorem pow_right {a x y : M} (h : SemiconjBy a x y) (n : ℕ) : SemiconjBy a (x ^ n) (y ^ n) := by
  induction n with
  | zero =>
    rw [pow_zero, pow_zero]
    exact SemiconjBy.one_right _
  | succ n ih =>
    rw [pow_succ, pow_succ]
    exact ih.mul_right h

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