intCast_mul_intCast_mul — Mathlib

English

If h is a semiconjugacy between a and x by y, then scaling by integers on both a and the inputs preserves semiconjugacy: SemiconjBy a x y implies SemiconjBy (m*a) (n*x) (n*y) for integers m,n.

Русский

Если h — полупривод между a и x по y, то умножение на целые числа на обе стороны сохраняет полупривод: SemiconjBy a x y влечёт SemiconjBy (m*a) (n*x) (n*y).

LaTeX

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

Lean4

theorem intCast_mul_intCast_mul (h : SemiconjBy a x y) (m n : ℤ) : SemiconjBy (m * a) (n * x) (n * y) := by simp [h]

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