instSMulℝ — Mathlib

English

When restricting the scalar action to the real scalars with a tower of scalars, the same evaluation rule holds: (n • f)(z) = n • f(z).

Русский

При ограничении скалярного действия до действительных скаляров через тензорную структуру действует то же правило: (n • f)(z) = n · f(z).

LaTeX

$$$$ (n \\cdot f)(z) = n \\cdot f(z). $$$$

Lean4

/-- Scalar multiplication by `ℝ`, valid without restrictions on the determinant. -/
instance instSMulℝ : SMul α (SlashInvariantForm Γ k) where
  smul c
    f :=
    { toFun := c • ↑f
      slash_action_eq' γ
        hγ := by
        rw [← smul_one_smul ℝ, ← smul_one_smul ℂ, smul_slash, Complex.real_smul, mul_one, σ_ofReal,
          slash_action_eqn _ _ hγ] }

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