of_linearEquiv — Mathlib

English

A module is flat iff it is preserved under linear equivalences.

Русский

Модуль плоский тогда и только тогда, когда он сохраняется под линейными эквивалентностями.

LaTeX

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

Lean4

/-- A `R`-module linearly equivalent to a flat `R`-module is flat. -/
theorem of_linearEquiv [Flat R M] (e : N ≃ₗ[R] M) : Flat R N :=
  of_retract e.toLinearMap e.symm (by simp)

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