mulSupport_inv

Mathlib.Algebra.Group.Support

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

English

The support of the inverse-valued function f is equal to the support of f (in a DivisionMonoid context).

Русский

Опора функции с обратной операцией равна опоре исходной функции (в контексте DivisionMonoid).

LaTeX

$$mulSupport f^{-1} = mulSupport f$$

Lean4

@[to_additive (attr := simp)]
theorem mulSupport_inv : mulSupport f⁻¹ = mulSupport f :=
  mulSupport_fun_inv f

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

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

Разделы

Аффилиация

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