of_inv

Mathlib.Topology.Algebra.InfiniteSum.Group

URI: https://scilib.ai/kg/mathlib#Multipliable.of_inv

English

If Multipliable (fun b ↦ (f b)⁻¹) along L, then Multipliable f along L.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem of_inv (hf : Multipliable (fun b ↦ (f b)⁻¹) L) : Multipliable f L := by simpa only [inv_inv] using hf.inv

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

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

Разделы

Аффилиация

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