mk_semiconjBy — Mathlib

English

For a unit u and x in M, SemiconjBy u (x) (u x u^{-1}) holds; i.e., a unit semiconjugates x to its conjugate under u.

Русский

Для единицы u и элемента x в M полусопряжение u сопрягает x с u x u^{-1}.

LaTeX

$$$$\forall u\in M^{\times},\forall x\in M:\ SemiconjBy (u) x (u x u^{-1}).$$$$

Lean4

/-- `a` semiconjugates `x` to `a * x * a⁻¹`. -/
@[to_additive /-- `a` semiconjugates `x` to `a + x + -a`. -/
    ]
theorem mk_semiconjBy (u : Mˣ) (x : M) : SemiconjBy (↑u) x (u * x * ↑u⁻¹) := by unfold SemiconjBy;
  rw [Units.inv_mul_cancel_right]

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