instOfIsDedekindDomainOfNoZeroSMulDivisors

English

If R is a Dedekind domain and NoZeroSMulDivisors holds for R-modules, then every such module M is flat.

Русский

Если R — Дедекиндова область и выполняется условие NoZeroSMulDivisors для модуля R, то любой такой модуль M плоский.

LaTeX

$$$Flat\\,R\\,M$$$

Lean4

instance [IsDedekindDomain R] [NoZeroSMulDivisors R M] : Flat R M :=
  by
  rw [IsDedekindDomain.flat_iff_torsion_eq_bot, ← Submodule.noZeroSMulDivisors_iff_torsion_eq_bot]
  infer_instance

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