# Algebraic Independence #

This file contains basic results on algebraic independence of a family of elements of an `R`-algebra

## References #

- Stacks: Transcendence

## Tags #

transcendence basis, transcendence degree, transcendence

source
def Algebra.trdeg (R : Type u_2) (A : Type v) [CommRing R] [CommRing A] [Algebra R A] :
Cardinal.{v}

The transcendence degree of a commutative algebra `A` over a commutative ring `R` is defined to be the maximal cardinality of an `R`-algebraically independent set in `A`.

Equations

- Algebra.trdeg R A = ⨆ (ι : { s : Set A // AlgebraicIndepOn R id s }), Cardinal.mk ↑↑ι

Instances For

source
theorem algebraicIndependent_iff_ker_eq_bot {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] :
AlgebraicIndependent R x ↔ RingHom.ker (MvPolynomial.aeval x).toRingHom = ⊥
source
@[simp]
theorem algebraicIndependent_empty_type_iff {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] [IsEmpty ι] :
AlgebraicIndependent R x ↔ Function.Injective ⇑(algebraMap R A)
source
instance instNonemptySubtypeSetAlgebraicIndepOnIdOfFaithfulSMul {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [FaithfulSMul R A] :
Nonempty { s : Set A // AlgebraicIndepOn R id s }
source
theorem AlgebraicIndependent.algebraMap_injective {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) :
Function.Injective ⇑(algebraMap R A)
source
theorem AlgebraicIndependent.linearIndependent {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) :
LinearIndependent R x
source
theorem AlgebraicIndependent.injective {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) [Nontrivial R] :
Function.Injective x
source
theorem AlgebraicIndependent.ne_zero {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) [Nontrivial R] (i : ι) :
x i ≠ 0
source
theorem AlgebraicIndependent.map {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {x : ι → A} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (hx : AlgebraicIndependent R x) {f : A →ₐ[R] A'} (hf_inj : Set.InjOn ⇑f ↑(Algebra.adjoin R (Set.range x))) :
AlgebraicIndependent R (⇑f ∘ x)
source
theorem AlgebraicIndependent.map' {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {x : ι → A} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (hx : AlgebraicIndependent R x) {f : A →ₐ[R] A'} (hf_inj : Function.Injective ⇑f) :
AlgebraicIndependent R (⇑f ∘ x)
source
theorem AlgebraicIndependent.aeval_of_algebraicIndependent {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) {f : ι → MvPolynomial ι R} (hf : AlgebraicIndependent R f) :
AlgebraicIndependent R fun (i : ι) => (MvPolynomial.aeval x) (f i)

If `x = {x_i : A | i : ι}` and `f = {f_i : MvPolynomial ι R | i : ι}` are algebraically independent over `R`, then `{f_i(x) | i : ι}` is also algebraically independent over `R`. For the partial converse, see `AlgebraicIndependent.of_aeval`.

source
theorem AlgebraicIndependent.of_aeval {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] {f : ι → MvPolynomial ι R} (H : AlgebraicIndependent R fun (i : ι) => (MvPolynomial.aeval x) (f i)) :
AlgebraicIndependent R f

If `{f_i(x) | i : ι}` is algebraically independent over `R`, then `{f_i : MvPolynomial ι R | i : ι}` is also algebraically independent over `R`. In fact, the `x = {x_i : A | i : ι}` is also transcendental over `R` provided that `R` is a field and `ι` is finite; the proof needs transcendence degree.

source
theorem isEmpty_algebraicIndependent {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (h : ¬Function.Injective ⇑(algebraMap R A)) :
IsEmpty { s : Set A // AlgebraicIndepOn R id s }
source
theorem trdeg_eq_zero_of_not_injective {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (h : ¬Function.Injective ⇑(algebraMap R A)) :
Algebra.trdeg R A = 0
source
theorem MvPolynomial.algebraicIndependent_X (σ : Type u_3) (R : Type u_4) [CommRing R] :
AlgebraicIndependent R X
source
theorem AlgHom.algebraicIndependent_iff {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {x : ι → A} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (f : A →ₐ[R] A') (hf : Function.Injective ⇑f) :
AlgebraicIndependent R (⇑f ∘ x) ↔ AlgebraicIndependent R x
source
theorem AlgebraicIndependent.of_subsingleton {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] [Subsingleton R] :
AlgebraicIndependent R x
source
theorem isTranscendenceBasis_iff_of_subsingleton {ι : Type u} {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [Subsingleton R] (x : ι → A) :
IsTranscendenceBasis R x ↔ Nonempty ι
source
theorem IsTranscendenceBasis.of_subsingleton {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] [Subsingleton R] [Nonempty ι] :
IsTranscendenceBasis R x
source
theorem trdeg_subsingleton {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [Subsingleton R] :
Algebra.trdeg R A = 1
source
theorem algebraicIndependent_adjoin {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hs : AlgebraicIndependent R x) :
AlgebraicIndependent R fun (i : ι) => ⟨x i, ⋯⟩
source
theorem AlgebraicIndependent.restrictScalars {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] {K : Type u_3} [CommRing K] [Algebra R K] [Algebra K A] [IsScalarTower R K A] (hinj : Function.Injective ⇑(algebraMap R K)) (ai : AlgebraicIndependent K x) :
AlgebraicIndependent R x

A set of algebraically independent elements in an algebra `A` over a ring `K` is also algebraically independent over a subring `R` of `K`.

source
theorem AlgebraicIndependent.of_ringHom_of_comp_eq {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] {S : Type u_3} {B : Type u_4} {FRS : Type u_5} {FAB : Type u_6} [CommRing S] [CommRing B] [Algebra S B] [FunLike FRS R S] [RingHomClass FRS R S] [FunLike FAB A B] [RingHomClass FAB A B] (f : FRS) (g : FAB) (H : AlgebraicIndependent S (⇑g ∘ x)) (hf : Function.Injective ⇑f) (h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)) :
AlgebraicIndependent R x
source
theorem AlgebraicIndependent.ringHom_of_comp_eq {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] {S : Type u_3} {B : Type u_4} {FRS : Type u_5} {FAB : Type u_6} [CommRing S] [CommRing B] [Algebra S B] [FunLike FRS R S] [RingHomClass FRS R S] [FunLike FAB A B] [RingHomClass FAB A B] (f : FRS) (g : FAB) (H : AlgebraicIndependent R x) (hf : Function.Surjective ⇑f) (hg : Function.Injective ⇑g) (h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)) :
AlgebraicIndependent S (⇑g ∘ x)
source
theorem algebraicIndependent_ringHom_iff_of_comp_eq {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] {S : Type u_3} {B : Type u_4} {FRS : Type u_5} {FAB : Type u_6} [CommRing S] [CommRing B] [Algebra S B] [EquivLike FRS R S] [RingEquivClass FRS R S] [FunLike FAB A B] [RingHomClass FAB A B] (f : FRS) (g : FAB) (hg : Function.Injective ⇑g) (h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)) :
AlgebraicIndependent S (⇑g ∘ x) ↔ AlgebraicIndependent R x
source
theorem algebraicIndependent_finset_map_embedding_subtype {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (s : Set A) (li : AlgebraicIndependent R Subtype.val) (t : Finset ↑s) :
AlgebraicIndependent R Subtype.val

Every finite subset of an algebraically independent set is algebraically independent.

source
theorem algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {n : ℕ} (H : ∀ (s : Finset A), (AlgebraicIndependent R fun (i : ↥s) => ↑i) → s.card ≤ n) (s : Set A) :
AlgebraicIndependent R Subtype.val → Cardinal.mk ↑s ≤ ↑n

If every finite set of algebraically independent element has cardinality at most `n`, then the same is true for arbitrary sets of algebraically independent elements.

source
theorem AlgebraicIndependent.restrict_of_comp_subtype {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] {s : Set ι} (hs : AlgebraicIndependent R (x ∘ Subtype.val)) :
AlgebraicIndependent R (s.restrict x)
source
theorem algebraicIndependent_empty_iff (R : Type u_2) (A : Type v) [CommRing R] [CommRing A] [Algebra R A] :
AlgebraicIndependent R Subtype.val ↔ Function.Injective ⇑(algebraMap R A)
source
theorem AlgebraicIndependent.to_subtype_range {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) :
AlgebraicIndependent R Subtype.val
source
theorem AlgebraicIndependent.to_subtype_range' {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) {t : Set A} (ht : Set.range x = t) :
AlgebraicIndependent R Subtype.val
source
theorem IsTranscendenceBasis.to_subtype_range {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : IsTranscendenceBasis R x) :
IsTranscendenceBasis R Subtype.val
source
theorem IsTranscendenceBasis.to_subtype_range' {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : IsTranscendenceBasis R x) {t : Set A} (ht : Set.range x = t) :
IsTranscendenceBasis R Subtype.val
source
theorem IsTranscendenceBasis.of_comp {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] {x : ι → A} (f : A →ₐ[R] A') (h : Function.Injective ⇑f) (H : IsTranscendenceBasis R (⇑f ∘ x)) :
IsTranscendenceBasis R x
source
theorem IsTranscendenceBasis.of_comp_algebraMap {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] [Algebra A A'] [IsScalarTower R A A'] [FaithfulSMul A A'] {x : ι → A} (H : IsTranscendenceBasis R (⇑(algebraMap A A') ∘ x)) :
IsTranscendenceBasis R x
source
theorem AlgEquiv.isTranscendenceBasis {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {x : ι → A} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (e : A ≃ₐ[R] A') (hx : IsTranscendenceBasis R x) :
IsTranscendenceBasis R (⇑e ∘ x)

Also see `IsTranscendenceBasis.algebraMap_comp` for the composition with a algebraic extension.

source
theorem AlgEquiv.isTranscendenceBasis_iff {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {x : ι → A} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (e : A ≃ₐ[R] A') :
IsTranscendenceBasis R (⇑e ∘ x) ↔ IsTranscendenceBasis R x
source
theorem AlgebraicIndependent.lift_cardinalMk_le_trdeg {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] [Nontrivial R] (hx : AlgebraicIndependent R x) :
Cardinal.lift.{v, u} (Cardinal.mk ι) ≤ Cardinal.lift.{u, v} (Algebra.trdeg R A)
source
theorem AlgebraicIndependent.cardinalMk_le_trdeg {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] [Nontrivial R] {ι : Type v} {x : ι → A} (hx : AlgebraicIndependent R x) :
Cardinal.mk ι ≤ Algebra.trdeg R A
source
theorem lift_trdeg_le_of_injective {R : Type u_2} {A : Type v} {A' : Type v'} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (f : A →ₐ[R] A') (hf : Function.Injective ⇑f) :
Cardinal.lift.{v', v} (Algebra.trdeg R A) ≤ Cardinal.lift.{v, v'} (Algebra.trdeg R A')
source
theorem trdeg_le_of_injective {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {A' : Type v} [CommRing A'] [Algebra R A'] (f : A →ₐ[R] A') (hf : Function.Injective ⇑f) :
Algebra.trdeg R A ≤ Algebra.trdeg R A'
source
theorem lift_trdeg_le_of_surjective {R : Type u_2} {A : Type v} {A' : Type v'} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (f : A →ₐ[R] A') (hf : Function.Surjective ⇑f) :
Cardinal.lift.{v, v'} (Algebra.trdeg R A') ≤ Cardinal.lift.{v', v} (Algebra.trdeg R A)
source
theorem trdeg_le_of_surjective {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {A' : Type v} [CommRing A'] [Algebra R A'] (f : A →ₐ[R] A') (hf : Function.Surjective ⇑f) :
Algebra.trdeg R A' ≤ Algebra.trdeg R A
source
theorem AlgEquiv.lift_trdeg_eq {R : Type u_2} {A : Type v} {A' : Type v'} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A'] (e : A ≃ₐ[R] A') :
Cardinal.lift.{v', v} (Algebra.trdeg R A) = Cardinal.lift.{v, v'} (Algebra.trdeg R A')
source
theorem AlgEquiv.trdeg_eq {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {A' : Type v} [CommRing A'] [Algebra R A'] (e : A ≃ₐ[R] A') :
Algebra.trdeg R A = Algebra.trdeg R A'
source
theorem algebraicIndependent_comp_subtype {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] {s : Set ι} :
AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ p ∈ MvPolynomial.supported R s, (MvPolynomial.aeval x) p = 0 → p = 0
source
theorem algebraicIndependent_subtype {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {s : Set A} :
AlgebraicIndependent R Subtype.val ↔ ∀ p ∈ MvPolynomial.supported R s, (MvPolynomial.aeval id) p = 0 → p = 0
source
theorem algebraicIndependent_of_finite {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (s : Set A) (H : ∀ t ⊆ s, t.Finite → AlgebraicIndependent R Subtype.val) :
AlgebraicIndependent R Subtype.val
source
theorem algebraicIndependent_of_finite_type {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (H : ∀ (t : Set ι), t.Finite → AlgebraicIndependent R fun (i : ↑t) => x ↑i) :
AlgebraicIndependent R x
source
theorem AlgebraicIndependent.image_of_comp {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_3} {ι' : Type u_4} (s : Set ι) (f : ι → ι') (g : ι' → A) (hs : AlgebraicIndependent R fun (x : ↑s) => g (f ↑x)) :
AlgebraicIndependent R fun (x : ↑(f '' s)) => g ↑x
source
theorem AlgebraicIndependent.image {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {ι : Type u_3} {s : Set ι} {f : ι → A} (hs : AlgebraicIndependent R fun (x : ↑s) => f ↑x) :
AlgebraicIndependent R fun (x : ↑(f '' s)) => ↑x
source
theorem algebraicIndependent_iUnion_of_directed {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {η : Type u_3} [Nonempty η] {s : η → Set A} (hs : Directed (fun (x1 x2 : Set A) => x1 ⊆ x2) s) (h : ∀ (i : η), AlgebraicIndependent R Subtype.val) :
AlgebraicIndependent R Subtype.val
source
theorem algebraicIndependent_sUnion_of_directed {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {s : Set (Set A)} (hsn : s.Nonempty) (hs : DirectedOn (fun (x1 x2 : Set A) => x1 ⊆ x2) s) (h : ∀ a ∈ s, AlgebraicIndependent R Subtype.val) :
AlgebraicIndependent R Subtype.val
source
theorem exists_maximal_algebraicIndependent {R : Type u_2} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] (s t : Set A) (hst : s ⊆ t) (hs : AlgebraicIndepOn R id s) :
∃ (u : Set A), s ⊆ u ∧ Maximal (fun (x : Set A) => AlgebraicIndepOn R id x ∧ x ⊆ t) u
source
theorem AlgebraicIndependent.repr_ker {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) :
RingHom.ker ↑hx.repr = ⊥
source
def AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) :
MvPolynomial (Option ι) R ≃+* Polynomial ↥(Algebra.adjoin R (Set.range x))

The isomorphism between `MvPolynomial (Option ι) R` and the polynomial ring over the algebra generated by an algebraically independent family.

Equations

- hx.mvPolynomialOptionEquivPolynomialAdjoin = (MvPolynomial.optionEquivLeft R ι).toRingEquiv.trans (Polynomial.mapEquiv hx.aevalEquiv.toRingEquiv)

Instances For

source
@[simp]
theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (y : MvPolynomial (Option ι) R) :
hx.mvPolynomialOptionEquivPolynomialAdjoin y = Polynomial.map (↑hx.aevalEquiv) ((MvPolynomial.aeval fun (o : Option ι) => o.elim Polynomial.X fun (s : ι) => Polynomial.C (MvPolynomial.X s)) y)
source
@[simp]
theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C' {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (r : R) :
Polynomial.C (hx.aevalEquiv (MvPolynomial.C r)) = Polynomial.C ((algebraMap R ↥(Algebra.adjoin R (Set.range x))) r)

`simp`-normal form of `mvPolynomialOptionEquivPolynomialAdjoin_C`

source
theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (r : R) :
hx.mvPolynomialOptionEquivPolynomialAdjoin (MvPolynomial.C r) = Polynomial.C ((algebraMap R ↥(Algebra.adjoin R (Set.range x))) r)
source
theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) :
hx.mvPolynomialOptionEquivPolynomialAdjoin (MvPolynomial.X none) = Polynomial.X
source
theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (i : ι) :
hx.mvPolynomialOptionEquivPolynomialAdjoin (MvPolynomial.X (some i)) = Polynomial.C (hx.aevalEquiv (MvPolynomial.X i))
source
theorem AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A] (hx : AlgebraicIndependent R x) (a : A) :
(↑(Polynomial.aeval a)).comp hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom = ↑(MvPolynomial.aeval fun (o : Option ι) => o.elim a x)
source
theorem algebraicIndependent_empty_type {ι : Type u} {A : Type v} {x : ι → A} [CommRing A] {K : Type u_3} [Field K] [Algebra K A] [IsEmpty ι] [Nontrivial A] :
AlgebraicIndependent K x
source
theorem algebraicIndependent_empty {A : Type v} [CommRing A] {K : Type u_3} [Field K] [Algebra K A] [Nontrivial A] :
AlgebraicIndependent K Subtype.val