inv_eq_one_divp

Mathlib.Algebra.Group.Units.Defs

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

English

The inverse of a unit equals the partial division of 1 by that unit: ↑u⁻¹ = 1 /ₚ u.

Русский

Обратное единицы равно частичному делению единицы на эту единицу: ↑u⁻¹ = 1 /ₚ u.

LaTeX

$$$\uparrow u^{-1} = 1 /ₚ u$$$

Lean4

theorem inv_eq_one_divp (u : αˣ) : ↑u⁻¹ = 1 /ₚ u := by rw [one_divp]

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

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

Разделы

Аффилиация

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