leOnePart_div_oneLePart

Mathlib.Algebra.Order.Group.PosPart

URI: https://scilib.ai/kg/mathlib#leOnePart_div_oneLePart

English

The division of the positive and the unit part equals the inverse of a: a⁻ᵐ / a⁺ᵐ = a⁻¹.

Русский

Деление положительной и единичной части даёт обратное элемента: a⁻ᵐ / a⁺ᵐ = a⁻¹.

LaTeX

$$$\frac{a^{-m}}{a^{+m}} = a^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem leOnePart_div_oneLePart (a : α) : a⁻ᵐ / a⁺ᵐ = a⁻¹ := by rw [← inv_div, oneLePart_div_leOnePart]

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

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

Разделы

Аффилиация

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