intCast_mul_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem intCast_mul_right (h : SemiconjBy a x y) (n : ℤ) : SemiconjBy a (n * x) (n * y) :=
  SemiconjBy.mul_right (Int.commute_cast _ _) h

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