injective

Mathlib.RingTheory.RingHom.FaithfullyFlat

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

English

FaithfullyFlat implies injectivity of the underlying ring map.

Русский

FaithfullyFlat предполагает инъективность сопоставления колец.

LaTeX

$$$\\operatorname{injective}(f) \\leftarrow\\operatorname{FaithfullyFlat}(f)$$$

Lean4

theorem injective (hf : f.FaithfullyFlat) : Function.Injective ⇑f :=
  by
  algebraize [f]
  exact FaithfulSMul.algebraMap_injective R S

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

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

Разделы

Аффилиация

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