mulSupport — Mathlib

English

The multiplicative support of a function f : ι → M is the set of indices x with f(x) ≠ 1.

Русский

Мультипликативная поддержка функции f : ι → M набирается из индексов x, для которых f(x) ≠ 1.

LaTeX

$$$ \\mathrm{mulSupport}(f) = \\{ x \\mid f(x) \\neq 1 \\} $$$

Lean4

/-- `mulSupport` of a function is the set of points `x` such that `f x ≠ 1`. -/
@[to_additive /-- `support` of a function is the set of points `x` such that `f x ≠ 0`. -/
    ]
def mulSupport (f : ι → M) : Set ι :=
  {x | f x ≠ 1}

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