value_smul — Mathlib

English

The value map respects scalar action: (φ • ψ).value = φ.value • ψ.value.

Русский

Значение жерма сохраняет скалярное умножение: (φ • ψ).value = φ.value • ψ.value.

LaTeX

$$(φ • ψ).value = φ.value • ψ.value$$

Lean4

theorem value_smul {α β : Type*} [SMul α β] (φ : Germ (𝓝 x) α) (ψ : Germ (𝓝 x) β) : (φ • ψ).value = φ.value • ψ.value :=
  Germ.inductionOn φ fun _ ↦ Germ.inductionOn ψ fun _ ↦ rfl

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