# mathlibdocumentation

ring_theory.localization.module

# Modules / vector spaces over localizations / fraction fields #

This file contains some results about vector spaces over the field of fractions of a ring.

## Main results #

• linear_independent.localization: b is linear independent over a localization of R if it is linear independent over R itself
• basis.localization: promote an R-basis b to an Rₛ-basis, where Rₛ is a localization of R
• linear_independent.iff_fraction_ring: b is linear independent over R iff it is linear independent over Frac(R)
theorem linear_independent.localization {R : Type u_1} (Rₛ : Type u_2) [comm_ring R] [comm_ring Rₛ] [ Rₛ] (S : submonoid R) [hT : Rₛ] {M : Type u_3} [ M] [module Rₛ M] [ Rₛ M] {ι : Type u_4} {b : ι → M} (hli : b) :
noncomputable def basis.localization {R : Type u_1} (Rₛ : Type u_2) [comm_ring R] [comm_ring Rₛ] [ Rₛ] (S : submonoid R) [hT : Rₛ] {M : Type u_3} [ M] [module Rₛ M] [ Rₛ M] {ι : Type u_4} (b : R M) :
Rₛ M

Promote a basis for M over R to a basis for M over the localization Rₛ

Equations
• b = _
theorem linear_independent.iff_fraction_ring (R : Type u_1) (K : Type u_2) [comm_ring R] [field K] [ K] [ K] {V : Type u_3} [ V] [ V] [ V] {ι : Type u_4} {b : ι → V} :