h — Mathlib · SciLib

English

Define h by conjugating g by τ: h(β) = τ g(β) τ^{-1}. Thus h is the conjugate of g by τ.

Русский

Определим h как конъюгацию g групповым элементом τ: h(β) = τ g(β) τ^{-1}. Следовательно, h есть конъугированная g по τ.

LaTeX

$$$$ h = \tau \circ g \circ \tau^{-1}. $$$$

Lean4

/-- Define `h : B ⟶ S(X')` to be `τ g τ⁻¹`
-/
def h : B →* SX' where
  toFun β := ((τ).symm.trans (g β)).trans τ
  map_one' := by
    ext
    simp
  map_mul' b1
    b2 := by
    ext
    simp

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