of_equiv — Mathlib

English

A linear equivalence between modules induces projectivity transfer: if M ≃ₗ[R] P and M is projective, then P is projective.

Русский

Линейное эквиверие между модулями переносит проективность: если M ≃ₗ[R] P и M проективен, то P проективен.

LaTeX

$$$$ \\text{If } M \\simeq P \\text{ and } M \\text{ is projective, then } P \\text{ is projective}. $$$$

Lean4

theorem of_equiv [Module.Projective R M] (e : M ≃ₗ[R] P) : Module.Projective R P :=
  Projective.of_split e.symm e.toLinearMap (by simp)

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