fieldEquivOfAlgEquivHom_apply

Mathlib.RingTheory.Localization.FractionRing

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

English

Compatibility of field equivalences with composition in the Hom-bundled setting.

Русский

Согласованность эквивалентностей полей с композицией в связке Hom.

LaTeX

$$$fieldEquivOfAlgEquivHom\_K^L \circ fieldEquivOfAlgEquivHom\_K^L = fieldEquivOfAlgEquivHom\_K^L$$$

Lean4

@[simp]
theorem fieldEquivOfAlgEquivHom_apply (f : B ≃ₐ[A] B) : fieldEquivOfAlgEquivHom K L f = fieldEquivOfAlgEquiv K L L f :=
  rfl

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

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

Разделы

Аффилиация

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