inv — Mathlib

English

If f is Multipliable along L, then the inverse function b ↦ (f b)⁻¹ is Multipliable along L.

Русский

Если f является Multipliable вдоль L, то инвертированная функция b ↦ (f b)⁻¹ также Multipliable вдоль L.

LaTeX

$$Multipliable f L → Multipliable (fun b => (f b)⁻¹) L$$

Lean4

@[to_additive]
theorem inv (hf : Multipliable f L) : Multipliable (fun b ↦ (f b)⁻¹) L :=
  hf.hasProd.inv.multipliable

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