inv_mem_inv

Mathlib.Data.Part

URI: https://scilib.ai/kg/mathlib#Part.inv_mem_inv

English

If ma ∈ a, then ma⁻¹ ∈ a⁻¹, provided α has inversion.

Русский

Если ma ∈ a, то ma⁻¹ ∈ a⁻¹ при условии существования обратного элемента в α.

LaTeX

$$$ ma^{-1} \in a^{-1} $$$

Lean4

@[to_additive]
theorem inv_mem_inv [Inv α] (a : Part α) (ma : α) (ha : ma ∈ a) : ma⁻¹ ∈ a⁻¹ := by simp [inv_def]; aesop

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

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

Разделы

Аффилиация

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