flat_iff_torsion_eq_bot — Mathlib

English

If R is a Dedekind domain, then an R-module M is flat iff it has no torsion.

Русский

Если R — Дедекиндова область, то R-модуль M плоский тогда и только тогда, когда у него отсутствует торсион.

LaTeX

$$$Flat\\,R\\,M \\iff torsion\\,R\\,M = \\bot$$$

Lean4

/-- If `R` is a Dedekind domain then an `R`-module is flat iff it has no torsion. -/
@[stacks 0AUW "(1)"]
theorem _root_.IsDedekindDomain.flat_iff_torsion_eq_bot [IsDedekindDomain R] : Flat R M ↔ torsion R M = ⊥ :=
  by
  apply flat_iff_torsion_eq_bot_of_valuationRing_localization_isMaximal
  exact fun P ↦ inferInstance

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