coe_inv — Mathlib

English

If U is a unitary element, then the inclusion of U^{-1} into the ambient ring equals the inverse of the inclusion of U, i.e., the embedding preserves inversion.

Русский

Пусть U — унитарный элемент. Тогда образ U^{-1} в окружающем кольце равен обратному образу U: вложение сохраняет обращение.

LaTeX

$$$\uparrow U^{-1} = (U^{-1} : R)$$$

Lean4

@[norm_cast]
theorem coe_inv (U : unitary R) : ↑U⁻¹ = (U⁻¹ : R) :=
  eq_inv_of_mul_eq_one_right <| coe_mul_star_self _

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