Theorems · Definition · field theory

AlgebraicIndependent.matroid

(R : Type u_1) →
  (A : Type w) →
    [inst : CommRing R] →
      [inst_1 : CommRing A] → [inst_2 : Algebra R A] → [FaithfulSMul R A] → [NoZeroDivisors A] → Matroid A

If R is a commutative ring and A is a commutative R-algebra with injective algebra map and no zero-divisors, then the R-algebraic independent subsets of A form a matroid.

Defined in

Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Cited by

17 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraFaithfulSMulNoZeroDivisors