Commit 2023-05-25 12:49 5ec08fd5

View on Github →

feat: port RingTheory.AlgebraicIndependent (#4263)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/AlgebraicIndependent.lean

added theorem AlgHom.algebraicIndependent_iff

added def AlgebraicIndependent.aevalEquiv

added theorem AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin

added theorem AlgebraicIndependent.aeval_comp_repr

added theorem AlgebraicIndependent.aeval_repr

added theorem AlgebraicIndependent.algebraMap_aevalEquiv

added theorem AlgebraicIndependent.algebraMap_injective

added theorem AlgebraicIndependent.coe_range

added theorem AlgebraicIndependent.comp

added theorem AlgebraicIndependent.eq_zero_of_aeval_eq_zero

added theorem AlgebraicIndependent.image

added theorem AlgebraicIndependent.image_of_comp

added theorem AlgebraicIndependent.isTranscendenceBasis_iff

added theorem AlgebraicIndependent.linearIndependent

added theorem AlgebraicIndependent.map'

added theorem AlgebraicIndependent.map

added theorem AlgebraicIndependent.mono

added def AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin

added theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C

added theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none

added theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some

added theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply

added theorem AlgebraicIndependent.ne_zero

added theorem AlgebraicIndependent.of_comp

added theorem AlgebraicIndependent.option_iff

added def AlgebraicIndependent.repr

added theorem AlgebraicIndependent.repr_ker

added theorem AlgebraicIndependent.restrictScalars

added theorem AlgebraicIndependent.restrict_of_comp_subtype

added theorem AlgebraicIndependent.to_subtype_range'

added theorem AlgebraicIndependent.to_subtype_range

added def AlgebraicIndependent

added theorem IsTranscendenceBasis.isAlgebraic

added def IsTranscendenceBasis

added theorem algebraicIndependent_adjoin

added theorem algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded

added theorem algebraicIndependent_comp_subtype

added theorem algebraicIndependent_empty

added theorem algebraicIndependent_empty_iff

added theorem algebraicIndependent_empty_type

added theorem algebraicIndependent_empty_type_iff

added theorem algebraicIndependent_equiv'

added theorem algebraicIndependent_equiv

added theorem algebraicIndependent_finset_map_embedding_subtype

added theorem algebraicIndependent_iUnion_of_directed

added theorem algebraicIndependent_iff

added theorem algebraicIndependent_iff_injective_aeval

added theorem algebraicIndependent_iff_ker_eq_bot

added theorem algebraicIndependent_image

added theorem algebraicIndependent_of_finite

added theorem algebraicIndependent_of_subsingleton

added theorem algebraicIndependent_sUnion_of_directed

added theorem algebraicIndependent_subtype

added theorem algebraicIndependent_subtype_range

added theorem exists_isTranscendenceBasis

added theorem exists_maximal_algebraicIndependent