Theorems · Theorem · commutative algebra

IsLocalization.mem_span_iff

∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {N : Type u_3} [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : Module S N] [IsScalarTower R S N] {x : N} {a : Set N},
  x ∈ Submodule.span S a ↔ ∃ y ∈ Submodule.span R a, ∃ z, x = IsLocalization.mk' S 1 z • y

Defined in

Mathlib.RingTheory.Localization.Submodule

Cited by

1 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraIsLocalizationAddCommMonoidModuleModuleIsScalarTower