smulZeroClassSet — Mathlib

English

If s is nonempty, then s · univ = univ.

Русский

Если s ненулево, то s · univ = univ.

LaTeX

$$$s \neq \emptyset \implies s \cdot \mathrm{univ} = \mathrm{univ}$$$

Lean4

/-- If scalar multiplication by elements of `α` sends `(0 : β)` to zero,
then the same is true for `(0 : Set β)`. -/
protected def smulZeroClassSet [Zero β] [SMulZeroClass α β] : SMulZeroClass α (Set β) where
  smul_zero _ := image_singleton.trans <| by rw [smul_zero, singleton_zero]

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