mul_bot

Mathlib.Algebra.Ring.Submonoid.Pointwise

URI: https://scilib.ai/kg/mathlib#AddSubmonoid.mul_bot

English

For any AddSubmonoid S, the product with the bottom submonoid is bottom: S * ⊥ = ⊥.

Русский

Для любого аддитивного подпмоноида S произведение с нижним подпмоном равно нижнему: S * ⊥ = ⊥.

LaTeX

$$$ S * \bot = \bot $$$

Lean4

@[simp]
theorem mul_bot (S : AddSubmonoid R) : S * ⊥ = ⊥ :=
  addSubmonoid_smul_bot S

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru