restrictScalars_fieldEquivOfAlgEquiv

Mathlib.RingTheory.Localization.FractionRing

URI: https://scilib.ai/kg/mathlib#IsFractionRing.restrictScalars_fieldEquivOfAlgEquiv

← MathLib Explorer

English

The symmetric of ringEquivOfRingEquiv h equals ringEquivOfRingEquiv h.symm.

Русский

Симметрия ringEquivOfRingEquiv h равна ringEquivOfRingEquiv h.symm.

LaTeX

$$$(\text{ringEquivOfRingEquiv } h)^{\mathrm{symm}} = \text{ringEquivOfRingEquiv } h^{\mathrm{symm}}$$$

Lean4

theorem restrictScalars_fieldEquivOfAlgEquiv (f : B ≃ₐ[A] C) :
    (fieldEquivOfAlgEquiv FA FB FC f).restrictScalars A = algEquivOfAlgEquiv f := by ext; rfl

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

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

Разделы

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

Аффилиация

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