mulSupport_mulSingle_one

Mathlib.Algebra.Notation.Support

URI: https://scilib.ai/kg/mathlib#Pi.mulSupport_mulSingle_one

English

The mulSupport of mulSingle i 1 is empty.

Русский

Опора mulSingle i 1 пустая.

LaTeX

$$$ \operatorname{mulSupport}(\mathrm{Pi}.\mathrm{mulSingle} i 1) = \emptyset $$$

Lean4

@[to_additive]
theorem mulSupport_mulSingle_one : mulSupport (mulSingle i (1 : M)) = ∅ := by simp

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

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

Разделы

Аффилиация

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