addSubmonoid_smul_bot — Mathlib

English

For any AddSubmonoid S of R, S • ⊥ = ⊥; i.e., scalar action by any element on the bottom submonoid yields bottom.

Русский

Для любого AddSubmonoid S ⊆ R выполняется S • ⊥ = ⊥; то есть скалярное действие на нижний подмонойд даёт нуль.

LaTeX

$$$S \cdot (\bot) = \bot$$$

Lean4

@[simp]
theorem addSubmonoid_smul_bot (S : AddSubmonoid R) : S • (⊥ : AddSubmonoid A) = ⊥ :=
  eq_bot_iff.2 <| smul_le.2 fun m _ n hn => by rw [AddSubmonoid.mem_bot] at hn ⊢; rw [hn, smul_zero]

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