init_zsmul — Mathlib

English

Init commutes with Z-scalar multiplication: init(n)(m • x) = init(n)(m • init(n)(x)).

Русский

Init сохраняет Z-скалярное умножение: init(n)(m • x) = init(n)(m • init(n)(x)).

LaTeX

$$$$\operatorname{init}_n(m \cdot x) = \operatorname{init}_n(m \cdot \operatorname{init}_n x).$$$$

Lean4

theorem init_zsmul (m : ℤ) (x : 𝕎 R) (n : ℕ) : init n (m • x) = init n (m • init n x) := by
  init_ring using fun p [Fact (Nat.Prime p)] n => wittZSMul_vars p m n

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