mulSupport_intCast — Mathlib

English

For α, β with AddGroupWithOne and CharZero β, the mulSupport of the constant function n : α → β is all of α if n ≠ 1.

Русский

Для β с AddGroupWithOne и CharZero, mulSupport константной функции n: α → β равно всему α если n ≠ 1.

LaTeX

$$$\\text{mulSupport}(n:\\alpha\\to\\beta)=\\text{univ}$, если $n\\neq 1$$$

Lean4

theorem mulSupport_intCast (hn : n ≠ 1) : mulSupport (n : α → β) = univ :=
  mulSupport_const <| Int.cast_ne_one.2 hn

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