flat_algebraMap_iff — Mathlib

English

A ring homomorphism is flat iff the target ring is flat as a module over the base ring.

Русский

Гомоморфизм кольца плоский тогда и только тогда, когда целевое кольцо плоско как модуль над базовым.

LaTeX

$$$(algebraMap\ R\ S).Flat \iff Module.Flat\ R\ S$$$

Lean4

theorem flat_algebraMap_iff {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] :
    (algebraMap R S).Flat ↔ Module.Flat R S := by rw [RingHom.Flat, toAlgebra_algebraMap]

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