mulSupport_fun_inv

Mathlib.Algebra.Group.Support

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

English

The support of f^{-1} equals the support of f for divisions monoids; i.e., the inverse operation preserves the support.

Русский

Опора f^{-1} равна опоре f в группе делений; тождество сохраняет опору.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem mulSupport_fun_inv : (mulSupport fun x => (f x)⁻¹) = mulSupport f :=
  ext fun _ => inv_ne_one

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

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

Разделы

Аффилиация

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