mul_invSelf

Mathlib.RingTheory.Localization.Away.Basic

URI: https://scilib.ai/kg/mathlib#IsLocalization.Away.mul_invSelf

← MathLib Explorer

English

The product of the image of x and its inverse in the away localization equals 1.

Русский

Произведение образа x и его обратного в away-локализации равно 1.

LaTeX

$$algebraMap R S x * invSelf x = 1$$

Lean4

@[simp]
theorem mul_invSelf : algebraMap R S x * invSelf x = 1 :=
  by
  convert IsLocalization.mk'_mul_mk'_eq_one (M := Submonoid.powers x) (S := S) _ 1
  symm
  apply IsLocalization.mk'_one

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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