instFreeSubtypeMemIdealOfFiniteOfNoZeroSMulDivisors

English

An instance asserting that a Subtype of a finite ideal is a free R-module when R is PID and NoZeroSMulDivisors holds.

Русский

Экземпляр, утверждающий, что подсубмодуль идеала является свободным R-модулем при PID и NoZeroSMulDivisors

LaTeX

$$$\\text{Module.Free } R (Subtype (\\text{mem } I))$$$

Lean4

instance {S : Type*} [CommRing S] [Algebra R S] {I : Ideal S} [hI₁ : Module.Finite R I] [hI₂ : NoZeroSMulDivisors R I] :
    Module.Free R I := by
  have : Module.Finite R (restrictScalars R I) := hI₁
  have : NoZeroSMulDivisors R (restrictScalars R I) := hI₂
  change Module.Free R (restrictScalars R I)
  exact Module.free_of_finite_type_torsion_free'

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