intCast_mul_left — Mathlib

English

If h is a semiconjugacy between a and y by x, then multiplying the left-hand side by n.cast preserves the semiconjugacy: h remains semiconjugating after scaling a by n.cast.

Русский

Если h — полупривод между a и y по x, то умножение левой части на n.cast сохраняет полупривод.

LaTeX

$$$ \forall {\alpha} [Ring \alpha] {a x y : \alpha},\ SemiconjBy a x y \rightarrow \forall (n : \mathbb{Z}),\ SemiconjBy (n \cdot a) x y.$$$

Lean4

@[simp]
theorem intCast_mul_left (h : SemiconjBy a x y) (n : ℤ) : SemiconjBy (n * a) x y :=
  SemiconjBy.mul_left (Int.cast_commute _ _) h

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