trans — Mathlib

English

If x is conjugate to y and y is conjugate to z, then x is conjugate to z.

Русский

Если x сопряжён к y, а y — к z, то x — к z.

LaTeX

$$$IsConjRoot(R, x, y) \land IsConjRoot(R, y, z) \Rightarrow IsConjRoot(R, x, z)$$$

Lean4

/-- If `y` is a conjugate root of `x` and `z` is a conjugate root of `y`, then `z` is a conjugate
root of `x`.
-/
@[trans]
theorem trans {x y z : A} (h₁ : IsConjRoot R x y) (h₂ : IsConjRoot R y z) : IsConjRoot R x z :=
  Eq.trans h₁ h₂

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