free_iff_set — Mathlib

English

Freeness of a module is equivalent to the existence of a basis indexed by some set.

Русский

Свободность модуля эквивалентна существованию базиса, индексированного некоторым множеством.

LaTeX

$$$$ \mathrm{Free}_R M \iff \exists S \subseteq M, \mathrm{Basis}(S,R,M) $$$$

Lean4

theorem free_iff_set : Free R M ↔ ∃ S : Set M, Nonempty (Basis S R M) :=
  ⟨fun _ ↦ Free.exists_set .., fun ⟨S, hS⟩ ↦ ⟨nonempty_sigma.2 ⟨S, hS⟩⟩⟩

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