equiv_iff — Mathlib

English

A module linearly equivalent to a flat module is flat, and conversely.

Русский

Модуль линейно эквивалентен плоскому модулю — тоже плоский; и наоборот.

LaTeX

$$Module.Flat R M ↔ Module.Flat R N for linear equivalence e: M ≃ₗ[R] N$$

Lean4

/-- If an `R`-module `M` is linearly equivalent to another `R`-module `N`, then `M` is flat
  if and only if `N` is flat. -/
theorem equiv_iff (e : M ≃ₗ[R] N) : Flat R M ↔ Flat R N :=
  ⟨fun _ ↦ of_linearEquiv e.symm, fun _ ↦ of_linearEquiv e⟩

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