semiconjBy_star_star_star — Mathlib

English

The relation SemiconjBy is preserved under star: SemiconjBy(star x)(star z)(star y) iff SemiconjBy x y z.

Русский

Отношение полуправосопряженности сохраняется под звездой: SemiconjBy(star x)(star z)(star y) эквивалентно SemiconjBy x y z.

LaTeX

$$$$ \operatorname{SemiconjBy}(\star x)(\star z)(\star y) \iff \operatorname{SemiconjBy}(x)(y)(z). $$$$

Lean4

@[simp]
theorem semiconjBy_star_star_star {x y z : R} : SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z := by
  simp_rw [SemiconjBy, ← star_mul, star_inj, eq_comm]

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