units_zpow_right — Mathlib

English

For units x,y and a in a monoid, SemiconjBy a x y implies SemiconjBy a (x^{m}) (y^{m}) for all integers m.

Русский

Для единиц x,y и элемента a в моноиде, если a полусопрягает x к y, то для всех целых m имеет место SemiconjBy a (x^{m}) (y^{m}).

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem units_zpow_right {a : M} {x y : Mˣ} (h : SemiconjBy a x y) : ∀ m : ℤ, SemiconjBy a ↑(x ^ m) ↑(y ^ m)
  | (n : ℕ) => by simp only [zpow_natCast, Units.val_pow_eq_pow_val, h, pow_right]
  | -[n+1] => by simp only [zpow_negSucc, Units.val_pow_eq_pow_val, units_inv_right, h, pow_right]

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