mulSupport_natCast

Mathlib.Algebra.Ring.CharZero

URI: https://scilib.ai/kg/mathlib#Function.mulSupport_natCast

English

For n ≠ 1, the mulSupport of the function n.cast is univ.

Русский

Для n ≠ 1 мультподдержка функции n.cast равна total.

LaTeX

$$$\operatorname{mulSupport}(n.cast) = \mathrm{univ}$$$

Lean4

theorem mulSupport_natCast (hn : n ≠ 1) : mulSupport (n : α → R) = univ :=
  mulSupport_const <| Nat.cast_ne_one.2 hn

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

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

Разделы

Аффилиация

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