Commit 2024-12-02 12:55 4662221b

View on Github →

chore(RingTheory): split AlgebraicIndependent.lean (#19606) As a follow-up to splitting RingTheory/Algebraic.lean, also split AlgebraicIndependent.lean. This PR creates the following new files:

AlgebraicIndependent/Defs.lean: definition of AlgebraicIndependent and IsTranscendenceBasis
AlgebraicIndependent/Basic.lean: basic results on AlgebraicIndependent
AlgebraicIndependent/TranscendenceBasis.lean: basic results on TranscendenceBasis
AlgebraicIndependent/Adjoin.lean: relating AlgebraicIndependent and IntermediateField.adjoin
AlgebraicIndependent/Transcendental.lean: relating AlgebraicIndependent, Transcendental and Algebraic
AlgebraicIndependent/RankAndCardinality.lean: about the rank/cardinality of TranscendenceBasises

Estimated changes

Modified Mathlib.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Classification.lean

Modified Mathlib/FieldTheory/SeparableDegree.lean

Deleted Mathlib/RingTheory/AlgebraicIndependent.lean

deleted theorem AlgHom.algebraicIndependent_iff

deleted theorem Algebra.Transcendental.rank_eq_cardinalMk

deleted def AlgebraicIndependent.aevalEquiv

deleted def AlgebraicIndependent.aevalEquivField

deleted theorem AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe

deleted theorem AlgebraicIndependent.aevalEquivField_apply_coe

deleted theorem AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin

deleted theorem AlgebraicIndependent.aeval_comp_repr

deleted theorem AlgebraicIndependent.aeval_of_algebraicIndependent

deleted theorem AlgebraicIndependent.aeval_repr

deleted theorem AlgebraicIndependent.algebraMap_aevalEquiv

deleted theorem AlgebraicIndependent.algebraMap_injective

deleted theorem AlgebraicIndependent.coe_range

deleted theorem AlgebraicIndependent.comp

deleted theorem AlgebraicIndependent.eq_zero_of_aeval_eq_zero

deleted theorem AlgebraicIndependent.image

deleted theorem AlgebraicIndependent.image_of_comp

deleted theorem AlgebraicIndependent.isEmpty_of_isAlgebraic

deleted theorem AlgebraicIndependent.isTranscendenceBasis_iff

deleted theorem AlgebraicIndependent.liftAlgHom_comp_reprField

deleted theorem AlgebraicIndependent.lift_reprField

deleted theorem AlgebraicIndependent.linearIndependent

deleted theorem AlgebraicIndependent.map'

deleted theorem AlgebraicIndependent.map

deleted theorem AlgebraicIndependent.mono

deleted def AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin

deleted theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C'

deleted theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C

deleted theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none

deleted theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some

deleted theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply

deleted theorem AlgebraicIndependent.ne_zero

deleted theorem AlgebraicIndependent.of_aeval

deleted theorem AlgebraicIndependent.of_comp

deleted theorem AlgebraicIndependent.of_ringHom_of_comp_eq

deleted theorem AlgebraicIndependent.option_iff

deleted theorem AlgebraicIndependent.polynomial_aeval_of_transcendental

deleted def AlgebraicIndependent.repr

deleted def AlgebraicIndependent.reprField

deleted theorem AlgebraicIndependent.repr_ker

deleted theorem AlgebraicIndependent.restrictScalars

deleted theorem AlgebraicIndependent.restrict_of_comp_subtype

deleted theorem AlgebraicIndependent.ringHom_of_comp_eq

deleted theorem AlgebraicIndependent.to_subtype_range'

deleted theorem AlgebraicIndependent.to_subtype_range

deleted theorem AlgebraicIndependent.transcendental

deleted def AlgebraicIndependent

deleted theorem IntermediateField.rank_sup_le

deleted theorem IsTranscendenceBasis.isAlgebraic

deleted theorem IsTranscendenceBasis.isAlgebraic_field

deleted theorem IsTranscendenceBasis.isEmpty_iff_isAlgebraic

deleted theorem IsTranscendenceBasis.lift_cardinalMk_eq_max_lift

deleted theorem IsTranscendenceBasis.lift_rank_eq_max_lift

deleted theorem IsTranscendenceBasis.nonempty_iff_transcendental

deleted def IsTranscendenceBasis

deleted theorem MvPolynomial.algebraicIndependent_X

deleted theorem MvPolynomial.algebraicIndependent_polynomial_aeval_X

deleted theorem algebraicIndependent_adjoin

deleted theorem algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded

deleted theorem algebraicIndependent_comp_subtype

deleted theorem algebraicIndependent_empty

deleted theorem algebraicIndependent_empty_iff

deleted theorem algebraicIndependent_empty_type

deleted theorem algebraicIndependent_empty_type_iff

deleted theorem algebraicIndependent_equiv'

deleted theorem algebraicIndependent_equiv

deleted theorem algebraicIndependent_finset_map_embedding_subtype

deleted theorem algebraicIndependent_iUnion_of_directed

deleted theorem algebraicIndependent_iff

deleted theorem algebraicIndependent_iff_injective_aeval

deleted theorem algebraicIndependent_iff_ker_eq_bot

deleted theorem algebraicIndependent_iff_transcendental

deleted theorem algebraicIndependent_image

deleted theorem algebraicIndependent_of_finite'

deleted theorem algebraicIndependent_of_finite

deleted theorem algebraicIndependent_of_finite_type'

deleted theorem algebraicIndependent_of_subsingleton

deleted theorem algebraicIndependent_ringHom_iff_of_comp_eq

deleted theorem algebraicIndependent_sUnion_of_directed

deleted theorem algebraicIndependent_subtype

deleted theorem algebraicIndependent_subtype_range

deleted theorem algebraicIndependent_unique_type_iff

deleted theorem exists_isTranscendenceBasis'

deleted theorem exists_isTranscendenceBasis

deleted theorem exists_maximal_algebraicIndependent

Created Mathlib/RingTheory/AlgebraicIndependent/Adjoin.lean

added def AlgebraicIndependent.aevalEquivField

added theorem AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe

added theorem AlgebraicIndependent.aevalEquivField_apply_coe

added theorem AlgebraicIndependent.liftAlgHom_comp_reprField

added theorem AlgebraicIndependent.lift_reprField

added def AlgebraicIndependent.reprField

Created Mathlib/RingTheory/AlgebraicIndependent/Basic.lean

added theorem AlgHom.algebraicIndependent_iff

added theorem AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin

added theorem AlgebraicIndependent.aeval_of_algebraicIndependent

added theorem AlgebraicIndependent.algebraMap_injective

added theorem AlgebraicIndependent.image

added theorem AlgebraicIndependent.image_of_comp

added theorem AlgebraicIndependent.linearIndependent

added theorem AlgebraicIndependent.map'

added theorem AlgebraicIndependent.map

added def AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin

added theorem AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C'

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_aeval

added theorem AlgebraicIndependent.of_ringHom_of_comp_eq

added theorem AlgebraicIndependent.repr_ker

added theorem AlgebraicIndependent.restrictScalars

added theorem AlgebraicIndependent.restrict_of_comp_subtype

added theorem AlgebraicIndependent.ringHom_of_comp_eq

added theorem AlgebraicIndependent.to_subtype_range'

added theorem AlgebraicIndependent.to_subtype_range

added theorem MvPolynomial.algebraicIndependent_X

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_finset_map_embedding_subtype

added theorem algebraicIndependent_iUnion_of_directed

added theorem algebraicIndependent_iff_ker_eq_bot

added theorem algebraicIndependent_of_finite

added theorem algebraicIndependent_of_subsingleton

added theorem algebraicIndependent_ringHom_iff_of_comp_eq

added theorem algebraicIndependent_sUnion_of_directed

added theorem algebraicIndependent_subtype

added theorem exists_maximal_algebraicIndependent

Created Mathlib/RingTheory/AlgebraicIndependent/Defs.lean

added def AlgebraicIndependent.aevalEquiv

added theorem AlgebraicIndependent.aeval_comp_repr

added theorem AlgebraicIndependent.aeval_repr

added theorem AlgebraicIndependent.algebraMap_aevalEquiv

added theorem AlgebraicIndependent.coe_range

added theorem AlgebraicIndependent.comp

added theorem AlgebraicIndependent.eq_zero_of_aeval_eq_zero

added theorem AlgebraicIndependent.mono

added theorem AlgebraicIndependent.of_comp

added def AlgebraicIndependent.repr

added def AlgebraicIndependent

added def IsTranscendenceBasis

added theorem algebraicIndependent_equiv'

added theorem algebraicIndependent_equiv

added theorem algebraicIndependent_iff

added theorem algebraicIndependent_iff_injective_aeval

added theorem algebraicIndependent_image

added theorem algebraicIndependent_subtype_range

Created Mathlib/RingTheory/AlgebraicIndependent/RankAndCardinality.lean

added theorem Algebra.Transcendental.rank_eq_cardinalMk

added theorem IntermediateField.rank_sup_le

added theorem IsTranscendenceBasis.lift_cardinalMk_eq_max_lift

added theorem IsTranscendenceBasis.lift_rank_eq_max_lift

Created Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean

added theorem AlgebraicIndependent.isTranscendenceBasis_iff

added theorem IsTranscendenceBasis.isAlgebraic

added theorem IsTranscendenceBasis.isAlgebraic_field

added theorem IsTranscendenceBasis.isEmpty_iff_isAlgebraic

added theorem IsTranscendenceBasis.nonempty_iff_transcendental

added theorem exists_isTranscendenceBasis'

added theorem exists_isTranscendenceBasis

Created Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean

added theorem AlgebraicIndependent.isEmpty_of_isAlgebraic

added theorem AlgebraicIndependent.option_iff

added theorem AlgebraicIndependent.polynomial_aeval_of_transcendental

added theorem AlgebraicIndependent.transcendental

added theorem MvPolynomial.algebraicIndependent_polynomial_aeval_X

added theorem algebraicIndependent_iff_transcendental

added theorem algebraicIndependent_of_finite'

added theorem algebraicIndependent_of_finite_type'

added theorem algebraicIndependent_unique_type_iff