respectsIso

Mathlib.RingTheory.RingHom.FaithfullyFlat

URI: https://scilib.ai/kg/mathlib#RingHom.FaithfullyFlat.respectsIso

English

FaithfullyFlat respects isomorphisms (base change compatibility).

Русский

FaithfullyFlat сохраняет изоморфии (совместимо с базовой сменой).

LaTeX

$$$\\operatorname{RespectsIso}(\\text{FaithfullyFlat})$$$

Lean4

theorem respectsIso : RespectsIso FaithfullyFlat :=
  stableUnderComposition.respectsIso (fun e ↦ .of_bijective e.bijective)

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

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

Разделы

Аффилиация

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