instSubalgebraToSubmodule

Mathlib.RingTheory.Flat.Basic

URI: https://scilib.ai/kg/mathlib#Module.Flat.instSubalgebraToSubmodule

English

If A is flat as an R-algebra, then A viewed as a submodule is flat over R.

Русский

Если A плоско как R-алгебра, то A как подмодуль над R плосок.

LaTeX

$$$[Flat\ R\ A] \Rightarrow Flat\ R\ A.toSubmodule$$$

Lean4

instance instSubalgebraToSubmodule {S : Type v} [Semiring S] [Algebra R S] (A : Subalgebra R S) [Flat R A] :
    Flat R A.toSubmodule :=
  ‹Flat R A›

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

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

Разделы

Аффилиация

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