of_free — Mathlib

English

If P has a basis b, then P is projective; equivalently, a basis provides a presentation giving a projective property.

Русский

Если у P есть базис b, то P проективен; эквивалентно тому, что базис обеспечивает презентацию с проективной характеристикой.

LaTeX

$$$$ \\text{If } b \\text{ is a basis of } P, \\text{ then } P \\text{ is projective}. $$$$

Lean4

instance (priority := 100) of_free [Module.Free R P] : Module.Projective R P :=
  .of_basis <| Module.Free.chooseBasis R P

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