faithfullyFlat_algebraMap_iff — Mathlib

English

For an algebra structure, (algebraMap R S).FaithfullyFlat is equivalent to Module.FaithfullyFlat R S.

Русский

Для алгебраической структуры (algebraMap R S).FaithfullyFlat эквивалентно Module.FaithfullyFlat R S.

LaTeX

$$$\\bigl( \\mathrm{algebraMap}\\;R\\;S \\bigr).\\operatorname{FaithfullyFlat} \\iff \\operatorname{Module.FaithfullyFlat} R S$$$

Lean4

theorem faithfullyFlat_algebraMap_iff [Algebra R S] : (algebraMap R S).FaithfullyFlat ↔ Module.FaithfullyFlat R S :=
  by
  simp only [FaithfullyFlat]
  congr!
  exact Algebra.algebra_ext _ _ fun _ ↦ rfl

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