free_of_finite_type_torsion_free'

English

An instance ensuring a free structure for a finite ideal under NoZeroSMulDivisors

Русский

Пример свободной структуры конечного идеала при NoZeroSMulDivisors

LaTeX

$$$\\mathbf{Free}(R, I)$ under hypotheses$$

Lean4

instance free_of_finite_type_torsion_free' [Module.Finite R M] [NoZeroSMulDivisors R M] : Module.Free R M :=
  by
  obtain ⟨n, b⟩ : Σ n, Basis (Fin n) R M := Module.basisOfFiniteTypeTorsionFree'
  exact Module.Free.of_basis b

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