Theorems · Theorem · linear algebra

IsLocalization.linearIndepOn_finsetIntegerMultiple

∀ {R : Type uR} {S : Type uS} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A : Type u_1}
  [inst_3 : CommRing A] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [IsScalarTower R S A] (M : Submonoid S)
  [inst_7 : IsLocalization M A] [FaithfulSMul S A] {s : Finset A},
  LinearIndepOn R id ↑s → ∀ [inst_9 : DecidableEq S], LinearIndepOn R id ↑(IsLocalization.finsetIntegerMultiple M s)

Defined in

Mathlib.LinearAlgebra.Dimension.Localization

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebraAlgebraIsScalarTowerIsLocalizationFaithfulSMulDecidableEq