Theorems · Definition · field theory
IsTranscendenceBasis
{ι : Type u_1} →
(R : Type u_3) → {A : Type u_5} → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → (ι → A) → PropA family is a transcendence basis if it is a maximal algebraically independent subset.
- Cited by
- 74 results in Mathlib
- Foundations
- Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- Set.rangeproof · cited by 4,705
- AlgebraicIndependentproof · cited by 120
- AlgebraicIndepOnproof · cited by 27
Cited by76
Results whose statement or proof uses this declaration.
- AlgebraicIndependent.matroidproof · cited by 17
- IsTranscendenceBasis.isAlgebraicstatement and proof · cited by 8
- IsTranscendenceBasis.lift_cardinalMk_eq_trdegstatement and proof · cited by 7
- exists_isTranscendenceBasisstatement and proof · cited by 5
- finTrdeg_iff_trdegproof · cited by 4
- IsTranscendenceBasis.isAlgebraic_fieldstatement and proof · cited by 3
- IsTranscendenceBasis.mvPolynomialstatement · cited by 3
- IsTranscendenceBasis.to_subtype_rangestatement and proof · cited by 3
- isTranscendenceBasis_equivstatement · cited by 3
- isTranscendenceBasis_iff_of_subsingletonstatement and proof · cited by 3
- isTranscendenceBasis_subtype_rangestatement · cited by 3
- AlgebraicIndependent.isTranscendenceBasis_iff_isAlgebraicstatement and proof · cited by 3