instMulZeroClassOfContinuousMul — Mathlib

English

If β is a MulZeroClass with ContinuousMul β, then C(α,β) is a MulZeroClass under pointwise multiplication; zero is the constant map to 0.

Русский

Если β — MulZeroClass с непрерывным умножением, то C(α,β) — MulZeroClass под точечным умножением; ноль — константная карта в ноль.

LaTeX

$$$\text{There is a zero map } 0: \alpha \to \beta,\ (f\cdot 0) = 0 = (0\cdot f).$$$

Lean4

instance [MulZeroClass β] [ContinuousMul β] : MulZeroClass C(α, β) :=
  coe_injective.mulZeroClass _ coe_zero coe_mul

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