coe_inv

Mathlib.Algebra.Algebra.Field

URI: https://scilib.ai/kg/mathlib#algebraMap.coe_inv

English

The algebra map preserves inverses: the image of r⁻¹ is the inverse of the image of r in A.

Русский

Изображение обратного элемента сохраняется: изображение r⁻¹ есть обратное изображению r в A.

LaTeX

$$$ \\uparrow r^{-1} = (\\uparrow r)^{-1} \\; \\text{in } A.$$$

Lean4

@[norm_cast]
theorem coe_inv (r : R) : ↑r⁻¹ = ((↑r)⁻¹ : A) :=
  map_inv₀ (algebraMap R A) r

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

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

Разделы

Аффилиация

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