Documentation Verification Report

Transcendental

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

Statistics

Metric	Count
Definitions `Transcendental`, `Transcendental`	2
Theorems `insert`, `insert_iff`, `adjoin_iff_disjoint`, `adjoin_of_disjoint`, `iff_adjoin_image`, `iff_adjoin_image_compl`, `iff_transcendental_adjoin_image`, `isEmpty_of_isAlgebraic`, `option_iff`, `option_iff_transcendental`, `polynomial_aeval_of_transcendental`, `sumElim`, `sumElim_comp`, `sumElim_iff`, `sumElim_of_tower`, `transcendental`, `transcendental_adjoin`, `transcendental_adjoin_iff`, `algebraicIndependent_polynomial_aeval_X`, `algebraicIndependent_iff_transcendental`, `algebraicIndependent_of_finite'`, `algebraicIndependent_of_finite_type'`, `algebraicIndependent_of_set_of_finite`, `algebraicIndependent_singleton_iff`, `algebraicIndependent_unique_type_iff`, `lift_trdeg_add_le`, `trdeg_add_le`, `trdeg_eq_zero`, `trdeg_eq_zero_iff`, `trdeg_ne_zero_iff`, `trdeg_pos`	31
Total	33

Algebra

Definitions

Name	Category	Theorems
`Transcendental` 📖	CompData	9 math math: `transcendental_ringHom_iff_of_comp_eq`, `Transcendental.ringHom_of_comp_eq`, `trdeg_ne_zero_iff`, `transcendental_of_subsingleton`, `transcendental_iff_not_isAlgebraic`, `Transcendental.of_ringHom_of_comp_eq`, `IsTranscendenceBasis.nonempty_iff_transcendental`, `RatFunc.transcendental`, `transcendental_def`

AlgebraicIndepOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`insert` 📖	mathematical	`AlgebraicIndepOn` `Transcendental` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.image` `Subalgebra.toCommRing` `CommRing.toRing` `Subalgebra.toAlgebra` `Ring.toSemiring` `Algebra.id`	`AlgebraicIndepOn` `Set` `Set.instInsert`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Function.Injective.nontrivial` `AlgebraicIndependent.algebraMap_injective` `insert_iff` `isAlgebraic_algebraMap` `SubsemiringClass.nontrivial` `Subalgebra.instSubsemiringClass` `Algebra.subset_adjoin`
`insert_iff` 📖	mathematical	`Set` `Set.instMembership`	`AlgebraicIndepOn` `Set` `Set.instInsert` `Transcendental` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.image` `Subalgebra.toCommRing` `CommRing.toRing` `Subalgebra.toAlgebra` `Ring.toSemiring` `Algebra.id`	—	`algebraicIndependent_equiv` `Set.image_eq_range` `AlgebraicIndependent.option_iff`

AlgebraicIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_iff_disjoint` 📖	mathematical	`AlgebraicIndependent`	`AlgebraicIndependent` `Set.Elem` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.image` `Set` `Set.instMembership` `Subalgebra.toCommRing` `Subalgebra.toAlgebra` `Algebra.id` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`of_not_not` `Set.not_disjoint_iff` `transcendental` `isAlgebraic_algebraMap` `SubsemiringClass.nontrivial` `Subalgebra.instSubsemiringClass` `Algebra.subset_adjoin` `adjoin_of_disjoint`
`adjoin_of_disjoint` 📖	mathematical	`AlgebraicIndependent` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`AlgebraicIndependent` `Set.Elem` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.image` `Set` `Set.instMembership` `Subalgebra.toCommRing` `Subalgebra.toAlgebra` `Algebra.id`	—	`comp` `iff_adjoin_image` `Disjoint.subset_compl_left` `Set.inclusion_injective`
`iff_adjoin_image` 📖	mathematical	—	`AlgebraicIndependent` `Set.Elem` `Set` `Set.instMembership` `AlgebraicIndepOn` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.image` `Subalgebra.toCommRing` `Subalgebra.toAlgebra` `Algebra.id` `Compl.compl` `Set.instCompl`	—	`Set.ext` `algebraicIndependent_equiv'` `sumElim_iff`
`iff_adjoin_image_compl` 📖	mathematical	—	`AlgebraicIndependent` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instMembership` `AlgebraicIndepOn` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.image` `Subalgebra.toCommRing` `Subalgebra.toAlgebra` `Algebra.id`	—	`compl_compl` `iff_adjoin_image`
`iff_transcendental_adjoin_image` 📖	mathematical	—	`AlgebraicIndependent` `Transcendental` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.image` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Subalgebra.toCommRing` `CommRing.toRing` `Subalgebra.toAlgebra` `Ring.toSemiring` `Algebra.id`	—	`iff_adjoin_image_compl` `algebraicIndependent_unique_type_iff`
`isEmpty_of_isAlgebraic` 📖	mathematical	`AlgebraicIndependent`	`IsEmpty`	—	`isEmpty_or_nonempty` `transcendental` `Algebra.IsAlgebraic.isAlgebraic`
`option_iff` 📖	mathematical	—	`AlgebraicIndependent` `Transcendental` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.range` `Subalgebra.toCommRing` `CommRing.toRing` `Subalgebra.toAlgebra` `Ring.toSemiring` `Algebra.id`	—	`comp` `Option.some_injective` `option_iff_transcendental`
`option_iff_transcendental` 📖	mathematical	`AlgebraicIndependent`	`AlgebraicIndependent` `Transcendental` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.range` `Subalgebra.toCommRing` `CommRing.toRing` `Subalgebra.toAlgebra` `Ring.toSemiring` `Algebra.id`	—	`algebraicIndependent_iff_injective_aeval` `transcendental_iff_injective` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.coe_toRingHom` `aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin` `RingHom.coe_comp` `Function.Injective.of_comp_iff'` `RingEquiv.bijective`
`polynomial_aeval_of_transcendental` 📖	mathematical	`AlgebraicIndependent` `Transcendental` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.ring` `CommRing.toRing` `Polynomial.algebraOfAlgebra` `Algebra.id`	`AlgebraicIndependent` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval`	—	`AlgHom.comp_apply` `Polynomial.algHom_ext` `Polynomial.aeval_X` `MvPolynomial.aeval_X` `aeval_of_algebraicIndependent` `MvPolynomial.algebraicIndependent_polynomial_aeval_X`
`sumElim` 📖	mathematical	`AlgebraicIndependent` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.range` `Subalgebra.toCommRing` `Subalgebra.toAlgebra` `Algebra.id`	`AlgebraicIndependent`	—	`sumElim_iff`
`sumElim_comp` 📖	mathematical	`AlgebraicIndependent`	`AlgebraicIndependent` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	`sumElim_of_tower` `map'` `algebraMap_injective` `Set.range_comp_subset_range`
`sumElim_iff` 📖	mathematical	—	`AlgebraicIndependent` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.range` `Subalgebra.toCommRing` `Subalgebra.toAlgebra` `Algebra.id`	—	`AddMonoidAlgebra.isScalarTower` `IsScalarTower.right` `IsScalarTower.subalgebra'` `MvPolynomial.algHom_ext` `MvPolynomial.aeval_X` `MvPolynomial.sumToIter_Xl` `MvPolynomial.map_X` `MvPolynomial.sumToIter_Xr` `MvPolynomial.map_C` `MvPolynomial.algHom_C` `comp` `Sum.inr_injective`
`sumElim_of_tower` 📖	mathematical	`AlgebraicIndependent` `Set` `Set.instHasSubset` `Set.range` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	`AlgebraicIndependent`	—	`algebraMap_injective` `Algebra.adjoin_le` `IsScalarTower.of_algebraMap_eq` `AlgEquiv.apply_symm_apply` `sumElim` `restrictScalars` `AlgEquiv.injective` `Subalgebra.inclusion_injective`
`transcendental` 📖	mathematical	`AlgebraicIndependent`	`Transcendental` `CommRing.toRing`	—	`comp` `Function.injective_of_subsingleton` `FinVec.map_eq` `algebraicIndependent_iff_transcendental`
`transcendental_adjoin` 📖	mathematical	`AlgebraicIndependent` `Set` `Set.instMembership`	`Transcendental` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.image` `Subalgebra.toCommRing` `CommRing.toRing` `Subalgebra.toAlgebra` `Ring.toSemiring` `Algebra.id`	—	`algebraicIndependent_singleton_iff` `Unique.instSubsingleton` `adjoin_of_disjoint` `Set.disjoint_singleton_right`
`transcendental_adjoin_iff` 📖	mathematical	`AlgebraicIndependent`	`Transcendental` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.image` `Subalgebra.toCommRing` `CommRing.toRing` `Subalgebra.toAlgebra` `Ring.toSemiring` `Algebra.id` `Set` `Set.instMembership`	—	`Set.disjoint_singleton_right` `algebraicIndependent_singleton_iff` `Unique.instSubsingleton` `adjoin_iff_disjoint`

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraicIndependent_polynomial_aeval_X` 📖	mathematical	`Transcendental` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.ring` `CommRing.toRing` `Polynomial.algebraOfAlgebra` `Algebra.id`	`AlgebraicIndependent` `MvPolynomial` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Polynomial.semiring` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Polynomial.algebraOfAlgebra` `Algebra.id` `AddMonoidAlgebra.algebra` `AlgHom.funLike` `Polynomial.aeval` `X` `AddMonoidAlgebra.commRing` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `AddCommMonoid.toAddMonoid`	—	`algebraicIndependent_of_finite_type'` `C_injective` `Algebra.adjoin_le_iff` `Set.image_subset_iff` `Set.mem_preimage` `Algebra.adjoin_mono` `Set.mem_image_of_mem` `Polynomial.aeval_mem_adjoin_singleton` `Transcendental.of_tower_top_of_subalgebra_le` `transcendental_supported_polynomial_aeval_X`

(root)

Definitions

Name	Category	Theorems
`Transcendental` 📖	MathDef	54 math math: `Polynomial.transcendental`, `AlgebraicIndependent.transcendental_adjoin_iff`, `RatFunc.transcendental_X`, `AlgebraicIndependent.transcendental_adjoin`, `Transcendental.of_tower_top`, `transcendental_iff_injective`, `transcendental_ringHom_iff_of_comp_eq`, `Transcendental.of_aeval`, `IsStronglyTranscendental.transcendental`, `MvPolynomial.transcendental_polynomial_aeval_X_iff`, `MvPolynomial.transcendental_supported_X_iff`, `Polynomial.transcendental_X`, `isStronglyTranscendental_iff_of_field`, `transcendental_aeval_iff`, `Transcendental.algebraicClosure`, `Algebra.IsIntegral.transcendental_iff`, `AlgebraicIndependent.option_iff_transcendental`, `Algebra.IsAlgebraic.transcendental_iff`, `transcendental_iff_ker_eq_bot`, `AlgebraicIndepOn.insert_iff`, `IsStronglyTranscendental.iff_of_isFractionRing`, `Transcendental.extendScalars_of_isIntegral`, `Transcendental.extendScalars`, `RatFunc.transcendental_of_ne_C`, `algebraicIndependent_singleton_iff`, `Transcendental.ringHom_of_comp_eq`, `transcendental_liouvilleNumber`, `Transcendental.subalgebraAlgebraicClosure`, `Transcendental.restrictScalars`, `is_transcendental_of_subsingleton`, `MvPolynomial.transcendental_polynomial_aeval_X`, `Transcendental.aeval`, `RatFunc.Luroth.transcendental_generator`, `Transcendental.pow`, `AlgebraicIndependent.option_iff`, `MvPolynomial.transcendental_X`, `Transcendental.of_ringHom_of_comp_eq`, `AlgebraicIndependent.transcendental`, `Algebra.Transcendental.transcendental`, `algebraicIndependent_iff_transcendental`, `Subalgebra.transcendental_iff_transcendental_val`, `Transcendental.of_tower_top_of_subalgebra_le`, `IntermediateField.transcendental_adjoin_iff`, `MvPolynomial.transcendental_supported_polynomial_aeval_X_iff`, `Liouville.transcendental`, `MvPolynomial.transcendental_supported_X`, `transcendental_iff`, `transcendental_algebraMap_iff`, `Algebra.transcendental_def`, `AlgebraicIndependent.iff_transcendental_adjoin_image`, `Transcendental.aeval_of_transcendental`, `Transcendental.integralClosure`, `algebraicIndependent_unique_type_iff`, `MvPolynomial.transcendental_supported_polynomial_aeval_X`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraicIndependent_iff_transcendental` 📖	mathematical	—	`AlgebraicIndependent` `Matrix.vecCons` `Matrix.vecEmpty` `Transcendental` `CommRing.toRing`	—	`Matrix.cons_val_fin_one`
`algebraicIndependent_of_finite'` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `Transcendental` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Subalgebra.toCommRing` `CommRing.toRing` `Subalgebra.toAlgebra` `Ring.toSemiring` `Algebra.id`	`AlgebraicIndependent` `Set` `Set.instMembership`	—	`algebraicIndependent_of_finite_type'` `Set.Finite.image` `AlgebraicIndependent.image` `Function.Injective.mem_set_image` `Subtype.val_injective`
`algebraicIndependent_of_finite_type'` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `Transcendental` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.image` `Subalgebra.toCommRing` `CommRing.toRing` `Subalgebra.toAlgebra` `Ring.toSemiring` `Algebra.id`	`AlgebraicIndependent`	—	`algebraicIndependent_of_set_of_finite` `algebraicIndependent_empty_type_iff` `Set.instIsEmptyElemEmptyCollection`
`algebraicIndependent_of_set_of_finite` 📖	mathematical	`AlgebraicIndependent` `Set.Elem` `Set` `Set.instMembership` `Transcendental` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.image` `Subalgebra.toCommRing` `CommRing.toRing` `Subalgebra.toAlgebra` `Ring.toSemiring` `Algebra.id`	`AlgebraicIndependent`	—	`algebraicIndependent_of_finite_type` `Set.Finite.induction_on_subset` `Set.Finite.diff` `AlgebraicIndependent.comp` `Set.union_empty` `Set.inclusion_injective` `Set.union_insert` `AlgebraicIndependent.option_iff_transcendental` `Set.image_eq_range` `Set.Finite.subset` `Set.union_subset` `Set.inter_subset_left` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.diff_subset` `Equiv.injective` `Set.inter_union_diff`
`algebraicIndependent_singleton_iff` 📖	mathematical	—	`AlgebraicIndependent` `Transcendental` `CommRing.toRing`	—	`algebraicIndependent_unique_type_iff`
`algebraicIndependent_unique_type_iff` 📖	mathematical	—	`AlgebraicIndependent` `Transcendental` `CommRing.toRing` `Unique.instInhabited`	—	`transcendental_iff_injective` `algebraicIndependent_iff_injective_aeval` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `MvPolynomial.algHom_ext` `Unique.instSubsingleton` `MvPolynomial.aeval_X` `MvPolynomial.rename_X` `MvPolynomial.eval₂_X` `Polynomial.aeval_X`
`lift_trdeg_add_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Cardinal.instAdd` `Cardinal.lift` `Algebra.trdeg`	—	`Cardinal.lift_iSup` `Cardinal.bddAbove_range` `small_subtype` `small_set` `UnivLE.small` `UnivLE.self` `Cardinal.ciSup_add_ciSup` `instNonemptySubtypeSetAlgebraicIndepOnIdOfFaithfulSMul` `univLE_of_max` `add_comm` `ciSup_le` `AlgebraicIndependent.sumElim_comp` `le_ciSup_of_le` `AlgebraicIndependent.to_subtype_range` `Cardinal.lift_umax` `Cardinal.mk_range_eq_of_injective` `AlgebraicIndependent.injective` `Cardinal.lift_id'` `le_refl`
`trdeg_add_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Cardinal.instAdd` `Algebra.trdeg`	—	`Cardinal.lift_id` `lift_trdeg_add_le`
`trdeg_eq_zero` 📖	mathematical	—	`Algebra.trdeg` `Cardinal` `Cardinal.instZero`	—	`bot_unique` `ciSup_le'` `AlgebraicIndependent.isEmpty_of_isAlgebraic` `Eq.le` `Cardinal.mk_eq_zero`
`trdeg_eq_zero_iff` 📖	mathematical	—	`Algebra.trdeg` `Cardinal` `Cardinal.instZero` `Algebra.IsAlgebraic` `CommRing.toRing`	—	`trdeg_eq_zero` `not_iff_not` `Algebra.transcendental_iff_not_isAlgebraic` `LT.lt.ne'` `trdeg_pos`
`trdeg_ne_zero_iff` 📖	mathematical	—	`Algebra.Transcendental` `CommRing.toRing`	—	`Algebra.transcendental_iff_not_isAlgebraic` `trdeg_eq_zero_iff`
`trdeg_pos` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Cardinal.instZero` `Algebra.trdeg`	—	`Algebra.Transcendental.transcendental` `LT.lt.trans_le` `zero_lt_one` `IsOrderedRing.toZeroLEOneClass` `Cardinal.isOrderedRing` `NeZero.charZero_one` `Cardinal.instCharZero` `le_ciSup_of_le` `Cardinal.bddAbove_range` `small_subtype` `small_set` `UnivLE.small` `UnivLE.self` `algebraicIndependent_unique_type_iff` `Cardinal.mk_fintype` `Fintype.card_unique` `Nat.cast_one` `instReflLe`

---

← Back to Index