isStableUnderBaseChange — Mathlib

English

FaithfullyFlat is stable under base change.

Русский

FaithfullyFlat устойчиво относительно базовых изменений.

LaTeX

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

Lean4

theorem isStableUnderBaseChange : IsStableUnderBaseChange FaithfullyFlat :=
  by
  refine .mk respectsIso (fun R S T _ _ _ _ _ _ ↦ show (algebraMap _ _).FaithfullyFlat from ?_)
  rw [faithfullyFlat_algebraMap_iff] at *
  infer_instance

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