inv_eq_one_divp'

Mathlib.Algebra.Group.Units.Basic

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

English

For a unit u in α, the image in α of the inverse of u equals the division by u, i.e., (1 / u) in α equals 1 /ₚ u.

Русский

Пусть u — единица α. Образ обратного элемента u в α равен делению единицы на u: (1/u) в α равно 1 /ₚ u.

LaTeX

$$$ (1 / u : α) = 1 /ₚ u $$$

Lean4

theorem inv_eq_one_divp' (u : αˣ) : ((1 / u : αˣ) : α) = 1 /ₚ u := by rw [one_div, one_divp]

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

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

Разделы

Аффилиация

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