Algebraic Independence #
This file defines algebraic independence of a family of elements of an R
algebra.
Main definitions #
AlgebraicIndependent
-AlgebraicIndependent R x
states the family of elementsx
is algebraically independent overR
, meaning that the canonical map out of the multivariable polynomial ring is injective.AlgebraicIndependent.aevalEquiv
- The canonical isomorphism from the polynomial ring to the subalgebra generated by an algebraic independent family.AlgebraicIndependent.repr
- The canonical map from the subalgebra generated by an algebraic independent family into the polynomial ring. It is the inverse ofAlgebraicIndependent.aevalEquiv
.IsTranscendenceBasis R x
- a familyx
is a transcendence basis overR
if it is a maximal algebraically independent subset.
Main results #
We show that algebraic independence is preserved under injective maps of the indices.
References #
AlgebraicIndependent R x
states the family of elements x
is algebraically independent over R
, meaning that the canonical
map out of the multivariable polynomial ring is injective.
Instances For
Alias of the forward direction of algebraicIndependent_subtype_range
.
Canonical isomorphism between polynomials and the subalgebra generated by algebraically independent elements.
Equations
Instances For
The canonical map from the subalgebra generated by an algebraic independent family into the polynomial ring.