Basic

📁 Source: Mathlib/RingTheory/AlgebraicIndependent/Basic.lean

Statistics

Metric	Count
Definitions `trdeg`, `mvPolynomialOptionEquivPolynomialAdjoin`	2
Theorems `isTranscendenceBasis`, `isTranscendenceBasis_iff`, `lift_trdeg_eq`, `trdeg_eq`, `algebraicIndependent_iff`, `aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin`, `aeval_of_algebraicIndependent`, `algebraMap_injective`, `cardinalMk_le_trdeg`, `image`, `image_of_comp`, `injective`, `lift_cardinalMk_le_trdeg`, `linearIndependent`, `map`, `map'`, `mvPolynomialOptionEquivPolynomialAdjoin_C`, `mvPolynomialOptionEquivPolynomialAdjoin_C'`, `mvPolynomialOptionEquivPolynomialAdjoin_X_none`, `mvPolynomialOptionEquivPolynomialAdjoin_X_some`, `mvPolynomialOptionEquivPolynomialAdjoin_apply`, `ne_zero`, `of_aeval`, `of_ringHom_of_comp_eq`, `of_subsingleton`, `repr_ker`, `restrictScalars`, `restrict_of_comp_subtype`, `ringHom_of_comp_eq`, `to_subtype_range`, `to_subtype_range'`, `of_comp`, `of_comp_algebraMap`, `of_subsingleton`, `to_subtype_range`, `to_subtype_range'`, `algebraicIndependent_X`, `algebraicIndependent_adjoin`, `algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded`, `algebraicIndependent_comp_subtype`, `algebraicIndependent_empty`, `algebraicIndependent_empty_iff`, `algebraicIndependent_empty_type`, `algebraicIndependent_empty_type_iff`, `algebraicIndependent_finset_map_embedding_subtype`, `algebraicIndependent_iUnion_of_directed`, `algebraicIndependent_iff_ker_eq_bot`, `algebraicIndependent_of_finite`, `algebraicIndependent_of_finite_type`, `algebraicIndependent_ringHom_iff_of_comp_eq`, `algebraicIndependent_sUnion_of_directed`, `algebraicIndependent_subtype`, `exists_maximal_algebraicIndependent`, `instNonemptySubtypeSetAlgebraicIndepOnIdOfFaithfulSMul`, `isEmpty_algebraicIndependent`, `isTranscendenceBasis_iff_of_subsingleton`, `lift_trdeg_le_of_injective`, `lift_trdeg_le_of_surjective`, `trdeg_eq_zero_of_not_injective`, `trdeg_le_of_injective`, `trdeg_le_of_surjective`, `trdeg_subsingleton`	62
Total	64

AlgEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTranscendenceBasis` 📖	mathematical	`IsTranscendenceBasis`	`IsTranscendenceBasis` `DFunLike.coe` `AlgEquiv` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `instFunLike`	—	`IsTranscendenceBasis.of_comp` `injective` `symm_apply_apply`
`isTranscendenceBasis_iff` 📖	mathematical	—	`IsTranscendenceBasis` `DFunLike.coe` `AlgEquiv` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `instFunLike`	—	`symm_apply_apply` `isTranscendenceBasis`
`lift_trdeg_eq` 📖	mathematical	—	`Cardinal.lift` `Algebra.trdeg`	—	`LE.le.antisymm` `lift_trdeg_le_of_injective` `injective` `lift_trdeg_le_of_surjective` `surjective`
`trdeg_eq` 📖	mathematical	—	`Algebra.trdeg`	—	`Cardinal.lift_id` `lift_trdeg_eq`

AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraicIndependent_iff` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `funLike`	`AlgebraicIndependent` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `funLike`	—	`AlgebraicIndependent.of_comp` `AlgebraicIndependent.map` `Function.Injective.injOn`

Algebra

Definitions

Name	Category	Theorems
`trdeg` 📖	CompOp	25 math math: `trdeg_eq_zero_of_not_injective`, `IsAlgebraic.trdeg_le_cardinalMk`, `trdeg_lt_aleph0`, `trdeg_eq_zero`, `lift_trdeg_le_of_injective`, `AlgebraicIndependent.matroid_cRank_eq`, `AlgEquiv.trdeg_eq`, `IsTranscendenceBasis.lift_cardinalMk_eq_trdeg`, `trdeg_add_eq`, `lift_trdeg_le_of_surjective`, `trdeg_add_le`, `trdeg_eq_iSup_cardinalMk_isTranscendenceBasis`, `AlgebraicIndependent.cardinalMk_le_trdeg`, `trdeg_pos`, `IsTranscendenceBasis.cardinalMk_eq_trdeg`, `lift_trdeg_add_eq`, `trdeg_subsingleton`, `trdeg_le_of_surjective`, `AlgebraicIndependent.lift_cardinalMk_le_trdeg`, `AlgEquiv.lift_trdeg_eq`, `lift_trdeg_add_le`, `MvPolynomial.trdeg_of_isDomain`, `trdeg_eq_zero_iff`, `trdeg_le_of_injective`, `Polynomial.trdeg_of_isDomain`

AlgebraicIndependent

Definitions

Name	Category	Theorems
`mvPolynomialOptionEquivPolynomialAdjoin` 📖	CompOp	5 math math: `mvPolynomialOptionEquivPolynomialAdjoin_C`, `aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin`, `mvPolynomialOptionEquivPolynomialAdjoin_X_some`, `mvPolynomialOptionEquivPolynomialAdjoin_X_none`, `mvPolynomialOptionEquivPolynomialAdjoin_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin` 📖	mathematical	`AlgebraicIndependent`	`RingHom.comp` `MvPolynomial` `CommRing.toCommSemiring` `Polynomial` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.range` `Subalgebra.toSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHomClass.toRingHom` `AlgHom` `Subalgebra.toCommSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Subalgebra.toAlgebra` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.aeval` `RingEquiv.toRingHom` `mvPolynomialOptionEquivPolynomialAdjoin` `AddMonoidAlgebra.semiring` `Finsupp.instAddMonoid` `AddMonoidAlgebra.algebra` `MvPolynomial.aeval`	—	`MvPolynomial.ringHom_ext` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `mvPolynomialOptionEquivPolynomialAdjoin_C` `MvPolynomial.aeval_C` `Polynomial.aeval_C` `IsScalarTower.algebraMap_apply` `IsScalarTower.subalgebra'` `IsScalarTower.right` `mvPolynomialOptionEquivPolynomialAdjoin_X_none` `MvPolynomial.aeval_X` `Polynomial.aeval_X` `mvPolynomialOptionEquivPolynomialAdjoin_X_some` `algebraMap_aevalEquiv`
`aeval_of_algebraicIndependent` 📖	mathematical	`AlgebraicIndependent` `MvPolynomial` `CommRing.toCommSemiring` `AddMonoidAlgebra.commRing` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `AddMonoidAlgebra.algebra` `CommSemiring.toSemiring` `Algebra.id` `AddCommMonoid.toAddMonoid`	`AlgebraicIndependent` `DFunLike.coe` `AlgHom` `MvPolynomial` `CommRing.toCommSemiring` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.aeval`	—	`algebraicIndependent_iff` `AlgHom.comp_apply` `MvPolynomial.aeval_comp_bind₁`
`algebraMap_injective` 📖	mathematical	`AlgebraicIndependent`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	`MvPolynomial.algHom_C` `Function.Injective.of_comp_iff` `algebraicIndependent_iff_injective_aeval` `MvPolynomial.C_injective`
`cardinalMk_le_trdeg` 📖	mathematical	`AlgebraicIndependent`	`Cardinal` `Cardinal.instLE` `Algebra.trdeg`	—	`Cardinal.lift_id` `lift_cardinalMk_le_trdeg`
`image` 📖	mathematical	`AlgebraicIndependent` `Set.Elem` `Set` `Set.instMembership`	`AlgebraicIndependent` `Set.Elem` `Set.image` `Set` `Set.instMembership`	—	`image_of_comp`
`image_of_comp` 📖	mathematical	`AlgebraicIndependent` `Set.Elem` `Set` `Set.instMembership`	`AlgebraicIndependent` `Set.Elem` `Set.image` `Set` `Set.instMembership`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Set.injOn_iff_injective` `Function.Injective.of_comp` `injective` `algebraicIndependent_equiv'`
`injective` 📖	—	`AlgebraicIndependent`	—	—	`LinearIndependent.injective` `linearIndependent`
`lift_cardinalMk_le_trdeg` 📖	mathematical	`AlgebraicIndependent`	`Cardinal` `Cardinal.instLE` `Cardinal.lift` `Algebra.trdeg`	—	`Cardinal.lift_mk_eq'` `injective` `Cardinal.lift_le` `le_ciSup_of_le` `Cardinal.bddAbove_range` `small_subtype` `small_set` `UnivLE.small` `UnivLE.self` `to_subtype_range` `le_rfl`
`linearIndependent` 📖	mathematical	`AlgebraicIndependent`	`LinearIndependent` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`linearIndependent_iff_injective_finsuppLinearCombination` `RingHomCompTriple.ids` `Finsupp.lhom_ext'` `LinearMap.ext_ring` `Finsupp.linearCombination_single` `one_smul` `MvPolynomial.aeval_X` `algebraicIndependent_iff_injective_aeval` `MvPolynomial.linearIndependent_X`
`map` 📖	mathematical	`AlgebraicIndependent` `Set.InjOn` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike` `SetLike.coe` `Subalgebra` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.range`	`AlgebraicIndependent` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	—	`MvPolynomial.algHom_ext` `MvPolynomial.aeval_X` `AlgHom.mem_range` `Set.mem_range_self` `MvPolynomial.aeval_rename` `Algebra.adjoin_eq_range`
`map'` 📖	mathematical	`AlgebraicIndependent` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	`AlgebraicIndependent` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	—	`map` `Function.Injective.injOn`
`mvPolynomialOptionEquivPolynomialAdjoin_C` 📖	mathematical	`AlgebraicIndependent`	`DFunLike.coe` `RingEquiv` `MvPolynomial` `CommRing.toCommSemiring` `Polynomial` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.range` `Subalgebra.toSemiring` `AddMonoidAlgebra.instMul` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Polynomial.instMul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Polynomial.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `mvPolynomialOptionEquivPolynomialAdjoin` `RingHom` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `RingHom.instFunLike` `MvPolynomial.C` `Polynomial.semiring` `Polynomial.C` `algebraMap` `Subalgebra.algebra`	—	`AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `MvPolynomial.algHom_C` `Polynomial.map_C` `mvPolynomialOptionEquivPolynomialAdjoin_C'`
`mvPolynomialOptionEquivPolynomialAdjoin_C'` 📖	mathematical	`AlgebraicIndependent`	`DFunLike.coe` `RingHom` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.range` `Polynomial` `Subalgebra.toSemiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `AlgEquiv` `MvPolynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `Subalgebra.algebra` `AlgEquiv.instFunLike` `aevalEquiv` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `MvPolynomial.C` `algebraMap`	—	`Subtype.val_injective` `MvPolynomial.algHom_C`
`mvPolynomialOptionEquivPolynomialAdjoin_X_none` 📖	mathematical	`AlgebraicIndependent`	`DFunLike.coe` `RingEquiv` `MvPolynomial` `CommRing.toCommSemiring` `Polynomial` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.range` `Subalgebra.toSemiring` `AddMonoidAlgebra.instMul` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Polynomial.instMul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Polynomial.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `mvPolynomialOptionEquivPolynomialAdjoin` `MvPolynomial.X` `Polynomial.X`	—	`AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `mvPolynomialOptionEquivPolynomialAdjoin_apply` `MvPolynomial.aeval_X` `Polynomial.map_X`
`mvPolynomialOptionEquivPolynomialAdjoin_X_some` 📖	mathematical	`AlgebraicIndependent`	`DFunLike.coe` `RingEquiv` `MvPolynomial` `CommRing.toCommSemiring` `Polynomial` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.range` `Subalgebra.toSemiring` `AddMonoidAlgebra.instMul` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Polynomial.instMul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Polynomial.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `mvPolynomialOptionEquivPolynomialAdjoin` `MvPolynomial.X` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `AlgEquiv` `AddMonoidAlgebra.semiring` `Finsupp.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `Subalgebra.algebra` `AlgEquiv.instFunLike` `aevalEquiv`	—	`AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `mvPolynomialOptionEquivPolynomialAdjoin_apply` `MvPolynomial.aeval_X` `Polynomial.map_C` `RingHom.coe_coe`
`mvPolynomialOptionEquivPolynomialAdjoin_apply` 📖	mathematical	`AlgebraicIndependent`	`DFunLike.coe` `RingEquiv` `MvPolynomial` `CommRing.toCommSemiring` `Polynomial` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.range` `Subalgebra.toSemiring` `AddMonoidAlgebra.instMul` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Polynomial.instMul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Polynomial.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `mvPolynomialOptionEquivPolynomialAdjoin` `Polynomial.map` `AddMonoidAlgebra.semiring` `Finsupp.instAddMonoid` `RingHomClass.toRingHom` `AlgEquiv` `AddMonoidAlgebra.algebra` `Algebra.id` `Subalgebra.algebra` `AlgEquiv.instFunLike` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `Semiring.toNonAssocSemiring` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instEquivLike` `AlgEquiv.instAlgEquivClass` `aevalEquiv` `AlgHom` `Polynomial.commSemiring` `AddMonoidAlgebra.commSemiring` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `Polynomial.algebraOfAlgebra` `AlgHom.funLike` `MvPolynomial.aeval` `Polynomial.X` `RingHom` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `MvPolynomial.X`	—	—
`ne_zero` 📖	—	`AlgebraicIndependent`	—	—	`LinearIndependent.ne_zero` `linearIndependent`
`of_aeval` 📖	mathematical	`AlgebraicIndependent` `DFunLike.coe` `AlgHom` `MvPolynomial` `CommRing.toCommSemiring` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.aeval`	`AlgebraicIndependent` `MvPolynomial` `CommRing.toCommSemiring` `AddMonoidAlgebra.commRing` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `AddMonoidAlgebra.algebra` `CommSemiring.toSemiring` `Algebra.id` `AddCommMonoid.toAddMonoid`	—	`algebraicIndependent_iff` `MvPolynomial.aeval_comp_bind₁` `AlgHom.comp_apply` `MvPolynomial.bind₁.eq_1` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`of_ringHom_of_comp_eq` 📖	mathematical	`AlgebraicIndependent` `DFunLike.coe` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap` `RingHomClass.toRingHom`	`AlgebraicIndependent`	—	`algebraicIndependent_iff` `MvPolynomial.aeval_eq_eval₂Hom` `MvPolynomial.eval₂Hom_map_hom` `MvPolynomial.map_aeval` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `MvPolynomial.map_injective` `RingHom.instRingHomClass`
`of_subsingleton` 📖	mathematical	—	`AlgebraicIndependent`	—	`algebraicIndependent_iff` `Unique.instSubsingleton`
`repr_ker` 📖	mathematical	`AlgebraicIndependent`	`RingHom.ker` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.range` `MvPolynomial` `RingHom` `Semiring.toNonAssocSemiring` `Subalgebra.toSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddMonoidAlgebra.semiring` `Finsupp.instAddMonoid` `RingHom.instFunLike` `RingHom.instRingHomClass` `RingHomClass.toRingHom` `AlgHom` `Subalgebra.algebra` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `repr` `Bot.bot` `Ideal` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `RingHom.instRingHomClass` `RingHom.injective_iff_ker_eq_bot` `AlgEquiv.injective`
`restrictScalars` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `AlgebraicIndependent`	`AlgebraicIndependent`	—	`MvPolynomial.ringHom_ext'` `RingHom.ext` `MvPolynomial.map_C` `Algebra.algebraMap_eq_smul_one` `MvPolynomial.algHom_C` `smul_assoc` `one_smul` `MvPolynomial.map_X` `MvPolynomial.aeval_X` `RingHom.coe_comp` `MvPolynomial.map_injective`
`restrict_of_comp_subtype` 📖	mathematical	`AlgebraicIndependent` `Set.Elem` `Set` `Set.instMembership`	`AlgebraicIndependent` `Set.Elem` `Set.restrict`	—	—
`ringHom_of_comp_eq` 📖	mathematical	`AlgebraicIndependent` `DFunLike.coe` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap` `RingHomClass.toRingHom`	`AlgebraicIndependent` `DFunLike.coe`	—	`algebraicIndependent_iff` `MvPolynomial.map_surjective` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.coe_coe` `MvPolynomial.map_aeval` `MvPolynomial.eval₂Hom_map_hom` `MvPolynomial.aeval_eq_eval₂Hom` `RingHom.instRingHomClass`
`to_subtype_range` 📖	mathematical	`AlgebraicIndependent`	`AlgebraicIndependent` `Set` `Set.instMembership` `Set.range`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `algebraicIndependent_subtype_range` `injective`
`to_subtype_range'` 📖	mathematical	`AlgebraicIndependent` `Set.range`	`AlgebraicIndependent` `Set` `Set.instMembership`	—	`to_subtype_range`

IsTranscendenceBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_comp` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike` `IsTranscendenceBasis`	`IsTranscendenceBasis`	—	`AlgHom.algebraicIndependent_iff` `algebraicIndependent_image` `Function.Injective.injOn` `Set.range_comp` `Set.image_mono` `Set.image_injective`
`of_comp_algebraMap` 📖	mathematical	`IsTranscendenceBasis` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	`IsTranscendenceBasis`	—	`of_comp` `FaithfulSMul.algebraMap_injective`
`of_subsingleton` 📖	mathematical	—	`IsTranscendenceBasis`	—	`isTranscendenceBasis_iff_of_subsingleton`
`to_subtype_range` 📖	mathematical	`IsTranscendenceBasis`	`IsTranscendenceBasis` `Set` `Set.instMembership` `Set.range`	—	`subsingleton_or_nontrivial` `isTranscendenceBasis_iff_of_subsingleton` `Set.instNonemptyRange` `isTranscendenceBasis_subtype_range` `AlgebraicIndependent.injective`
`to_subtype_range'` 📖	mathematical	`IsTranscendenceBasis` `Set.range`	`IsTranscendenceBasis` `Set` `Set.instMembership`	—	`to_subtype_range`

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraicIndependent_X` 📖	mathematical	—	`AlgebraicIndependent` `MvPolynomial` `CommRing.toCommSemiring` `X` `AddMonoidAlgebra.commRing` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `AddMonoidAlgebra.algebra` `CommSemiring.toSemiring` `Algebra.id` `AddCommMonoid.toAddMonoid`	—	`AlgebraicIndependent.eq_1` `aeval_X_left`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraicIndependent_adjoin` 📖	mathematical	`AlgebraicIndependent`	`AlgebraicIndependent` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.range` `Algebra.subset_adjoin` `Set.mem_range_self` `Subalgebra.toCommRing` `Subalgebra.algebra`	—	`AlgebraicIndependent.of_comp` `Algebra.subset_adjoin` `Set.mem_range_self`
`algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded` 📖	mathematical	`Finset.card` `AlgebraicIndependent` `Set` `Set.instMembership`	`Cardinal` `Cardinal.instLE` `Set.Elem` `Cardinal.instNatCast`	—	`Cardinal.card_le_of` `Finset.card_map` `algebraicIndependent_finset_map_embedding_subtype`
`algebraicIndependent_comp_subtype` 📖	mathematical	—	`AlgebraicIndependent` `Set.Elem` `Set` `Set.instMembership` `MvPolynomial` `CommRing.toCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Finsupp` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	`MvPolynomial.algHom_ext` `MvPolynomial.aeval_X` `MvPolynomial.rename_X` `injective_iff_map_eq_zero'` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `MvPolynomial.rename_injective` `Subtype.val_injective` `MvPolynomial.supported_eq_range_rename`
`algebraicIndependent_empty` 📖	mathematical	—	`AlgebraicIndependent` `Set` `Set.instMembership` `Set.instEmptyCollection` `Field.toCommRing`	—	`algebraicIndependent_empty_type` `Set.instIsEmptyElemEmptyCollection`
`algebraicIndependent_empty_iff` 📖	mathematical	—	`AlgebraicIndependent` `Set` `Set.instMembership` `Set.instEmptyCollection` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	`Set.instIsEmptyElemEmptyCollection`
`algebraicIndependent_empty_type` 📖	mathematical	—	`AlgebraicIndependent` `Field.toCommRing`	—	`algebraicIndependent_empty_type_iff` `RingHom.injective` `DivisionRing.isSimpleRing`
`algebraicIndependent_empty_type_iff` 📖	mathematical	—	`AlgebraicIndependent` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	`algebraicIndependent_iff_injective_aeval` `MvPolynomial.aeval_injective_iff_of_isEmpty`
`algebraicIndependent_finset_map_embedding_subtype` 📖	mathematical	`AlgebraicIndependent` `Set` `Set.instMembership`	`AlgebraicIndependent` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.map` `Set` `Set.instMembership` `Function.Embedding.subtype`	—	`Finset.mem_map` `AlgebraicIndependent.comp`
`algebraicIndependent_iUnion_of_directed` 📖	mathematical	`Directed` `Set` `Set.instHasSubset` `AlgebraicIndependent` `Set.instMembership`	`AlgebraicIndependent` `Set` `Set.instMembership` `Set.iUnion`	—	`algebraicIndependent_of_finite` `Set.finite_subset_iUnion` `Directed.finset_le` `Set.instIsTransSubset` `AlgebraicIndependent.mono` `Set.Subset.trans` `Set.iUnion₂_subset` `Set.Finite.mem_toFinset`
`algebraicIndependent_iff_ker_eq_bot` 📖	mathematical	—	`AlgebraicIndependent` `RingHom.ker` `MvPolynomial` `CommRing.toCommSemiring` `RingHom` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `RingHom.instFunLike` `RingHom.instRingHomClass` `AlgHom.toRingHom` `AddMonoidAlgebra.algebra` `Algebra.id` `MvPolynomial.aeval` `Bot.bot` `Ideal` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`RingHom.injective_iff_ker_eq_bot` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`algebraicIndependent_of_finite` 📖	mathematical	`AlgebraicIndependent` `Set` `Set.instMembership`	`AlgebraicIndependent` `Set` `Set.instMembership`	—	`algebraicIndependent_subtype` `MvPolynomial.mem_supported` `Finset.finite_toSet`
`algebraicIndependent_of_finite_type` 📖	mathematical	`AlgebraicIndependent` `Set.Elem` `Set` `Set.instMembership`	`AlgebraicIndependent`	—	`injective_iff_map_eq_zero` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `algebraicIndependent_comp_subtype` `Finset.finite_toSet` `MvPolynomial.mem_supported_vars`
`algebraicIndependent_ringHom_iff_of_comp_eq` 📖	mathematical	`DFunLike.coe` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap` `RingHomClass.toRingHom` `EquivLike.toFunLike` `RingEquivClass.toRingHomClass`	`AlgebraicIndependent` `DFunLike.coe`	—	`RingEquivClass.toRingHomClass` `AlgebraicIndependent.of_ringHom_of_comp_eq` `EquivLike.injective` `AlgebraicIndependent.ringHom_of_comp_eq` `EquivLike.surjective`
`algebraicIndependent_sUnion_of_directed` 📖	mathematical	`Set.Nonempty` `Set` `DirectedOn` `Set.instHasSubset` `AlgebraicIndependent` `Set.instMembership`	`AlgebraicIndependent` `Set` `Set.instMembership` `Set.sUnion`	—	`Set.sUnion_eq_iUnion` `algebraicIndependent_iUnion_of_directed` `Set.Nonempty.to_subtype` `DirectedOn.directed_val`
`algebraicIndependent_subtype` 📖	mathematical	—	`AlgebraicIndependent` `Set` `Set.instMembership` `MvPolynomial` `CommRing.toCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Finsupp` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	`algebraicIndependent_comp_subtype`
`exists_maximal_algebraicIndependent` 📖	mathematical	`Set` `Set.instHasSubset` `AlgebraicIndepOn`	`Set` `Set.instHasSubset` `Maximal` `Set.instLE` `AlgebraicIndepOn`	—	`zorn_subset_nonempty` `algebraicIndependent_sUnion_of_directed` `IsChain.directedOn` `Set.instReflSubset` `Set.subset_sUnion_of_mem`
`instNonemptySubtypeSetAlgebraicIndepOnIdOfFaithfulSMul` 📖	mathematical	—	`Set` `AlgebraicIndepOn`	—	`algebraicIndependent_empty_type_iff` `Set.instIsEmptyElemEmptyCollection` `FaithfulSMul.algebraMap_injective`
`isEmpty_algebraicIndependent` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	`IsEmpty` `Set` `AlgebraicIndepOn`	—	`AlgebraicIndependent.algebraMap_injective`
`isTranscendenceBasis_iff_of_subsingleton` 📖	mathematical	—	`IsTranscendenceBasis`	—	`Module.subsingleton` `AlgebraicIndependent.of_subsingleton` `Set.range_eq_empty` `instIsEmptyFalse` `HasSubset.Subset.antisymm` `Set.instAntisymmSubset`
`lift_trdeg_le_of_injective` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	`Cardinal` `Cardinal.instLE` `Cardinal.lift` `Algebra.trdeg`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `trdeg_subsingleton` `Cardinal.lift_one` `instReflLe` `Algebra.trdeg.eq_1` `Cardinal.lift_iSup` `Cardinal.bddAbove_range` `small_subtype` `small_set` `UnivLE.small` `UnivLE.self` `ciSup_le'` `AlgebraicIndependent.lift_cardinalMk_le_trdeg` `AlgebraicIndependent.map'`
`lift_trdeg_le_of_surjective` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	`Cardinal` `Cardinal.instLE` `Cardinal.lift` `Algebra.trdeg`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `trdeg_subsingleton` `Cardinal.lift_one` `instReflLe` `Algebra.trdeg.eq_1` `Cardinal.lift_iSup` `Cardinal.bddAbove_range` `small_subtype` `small_set` `UnivLE.small` `UnivLE.self` `ciSup_le'` `AlgebraicIndependent.lift_cardinalMk_le_trdeg` `Zero.instNonempty` `AlgebraicIndependent.of_comp` `Function.invFun_eq`
`trdeg_eq_zero_of_not_injective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	`Algebra.trdeg` `Cardinal` `Cardinal.instZero`	—	`isEmpty_algebraicIndependent` `Algebra.trdeg.eq_1` `ciSup_of_empty` `bot_eq_zero` `Cardinal.canonicallyOrderedAdd`
`trdeg_le_of_injective` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	`Cardinal` `Cardinal.instLE` `Algebra.trdeg`	—	`Cardinal.lift_id` `lift_trdeg_le_of_injective`
`trdeg_le_of_surjective` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	`Cardinal` `Cardinal.instLE` `Algebra.trdeg`	—	`Cardinal.lift_id` `lift_trdeg_le_of_surjective`
`trdeg_subsingleton` 📖	mathematical	—	`Algebra.trdeg` `Cardinal` `Cardinal.instOne`	—	`Module.subsingleton` `LE.le.antisymm` `ciSup_le'` `Set.subsingleton_of_subsingleton` `le_ciSup_of_le` `Cardinal.bddAbove_range` `small_subtype` `small_set` `UnivLE.small` `UnivLE.self` `AlgebraicIndependent.of_subsingleton` `Cardinal.mk_fintype` `Fintype.card_unique` `Nat.cast_one` `instReflLe`

---

← Back to Index