Defs

📁 Source: Mathlib/RingTheory/Algebraic/Defs.lean

Statistics

Metric	Count
Definitions IsAlgebraic, IsAlgebraic, IsAlgebraic	3
Theorems isAlgebraic, transcendental, isAlgebraic_def, isAlgebraic_iff, nontrivial_of_isAlgebraic, transcendental_def, transcendental_iff_not_isAlgebraic, isAlgebraic_iff, transcendental_iff	9
Total	12

Algebra

Definitions

Name	Category	Theorems
IsAlgebraic 📖	CompData	78 math math: AlgebraicIndependent.isTranscendenceBasis_iff_isAlgebraic, IsAlgebraic.of_ringHom_of_comp_eq, IntermediateField.isAlgebraic_tower_bot, instIsAlgebraicResidueFieldOfIsIntegral, IsAlgebraic.isAlgebraic_iff_bot, AlgEquiv.isAlgebraic, IsIntegral.isAlgebraic, IntermediateField.algebraAdjoinAdjoin.instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin, Subalgebra.algebra_isAlgebraic_bot_right, IsAlgebraic.tensorProduct, Subalgebra.algebra_isAlgebraic_bot_left_iff, IntermediateField.isAlgebraic_adjoin_iff_top, IsAlgebraic.tower_top, algebraicClosure.isAlgebraic, instIsAlgebraicPolynomialOfNoZeroDivisors_1, AlgebraicIndependent.matroid_spanning_iff, Field.isAlgebraic_of_finite_intermediateField, Subalgebra.algebra_isAlgebraic_of_algebra_isAlgebraic_bot_left, IsAlgebraic.of_finite, IsAlgebraic.trans, IntermediateField.isAlgebraic_adjoin, IsTranscendenceBasis.isAlgebraic_field, isAlgebraic_iff_isIntegral, IsPushout.isAlgebraic, IntermediateField.isAlgebraic_tower_top, instIsAlgebraicQuotientIdealResidueField, transcendental_iff_not_isAlgebraic, IsTranscendenceBasis.isAlgebraic_iff, IsAlgebraic.of_isIntegralClosure, IsAlgebraic.ringHom_of_comp_eq, IsAlgebraic.extendScalars, IntermediateField.isAlgebraic_adjoin_iff_isAlgebraic, PadicAlgCl.isAlgebraic, instIsAlgebraicMvPolynomialOfNoZeroDivisors, IntermediateField.isAlgebraic_adjoin_pair, isAlgebraic_ringHom_iff_of_comp_eq, instIsAlgebraicPolynomialOfNoZeroDivisors, Field.exists_primitive_element_iff_finite_intermediateField, Polynomial.IsSplittingField.IsScalarTower.isAlgebraic, isAlgebraic_iff, AlgEquiv.isAlgebraic_iff, isAlgebraic_iff_exists_isTranscendenceBasis_subset, isAlgebraic_def, IsSeparable.isAlgebraic, separableClosure.isAlgebraic, IsIntegral.isAlgebraic_iff_top, algebraicClosure.eq_top_iff, IsAlgClosure.isAlgebraic, TensorProduct.isAlgebraic_of_isField, IntermediateField.isAlgebraic_adjoin_simple, IsTranscendenceBasis.isEmpty_iff_isAlgebraic, Normal.toIsAlgebraic, perfectClosure.isAlgebraic, IsIntegral.trans_isAlgebraic, AlgebraicClosure.isAlgebraic, instIsAlgebraicMvPolynomialOfNoZeroDivisors_1, IsAlgebraic.isAlgebraic_iff_top, le_algebraicClosure_iff, IsFractionRing.isAlgebraic_iff', IsPurelyInseparable.isAlgebraic, isAlgebraic_of_isFractionRing, NumberField.isAlgebraic, IsAlgebraic.trans_isIntegral, isAlgClosure_iff, IsFractionRing.comap_isAlgebraic_iff, IsPushout.isAlgebraic', IsAlgebraic.tower_bot_of_injective, IsAlgebraic.of_injective, Subalgebra.isAlgebraic_iff, IntermediateField.isAlgebraic_adjoin_iff_bot, IsTranscendenceBasis.isAlgebraic, IsAlgebraic.tower_bot, isAlgebraic_of_not_injective, instIsAlgebraicSubtypeMemSubalgebraAlgebraicClosure, trdeg_eq_zero_iff, NumberField.instIsAlgebraicSubtypeMemSubfield, isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic, IsLocalization.isAlgebraic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAlgebraic_def 📖	mathematical	—	IsAlgebraic IsAlgebraic	—	—
isAlgebraic_iff 📖	mathematical	—	IsAlgebraic Subalgebra.IsAlgebraic Top.top Subalgebra CommRing.toCommSemiring Ring.toSemiring OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
nontrivial_of_isAlgebraic 📖	mathematical	—	Nontrivial	—	IsAlgebraic.isAlgebraic Polynomial.Nontrivial.of_polynomial_ne
transcendental_def 📖	mathematical	—	Transcendental Transcendental	—	—
transcendental_iff_not_isAlgebraic 📖	mathematical	—	Transcendental IsAlgebraic	—	—

Algebra.IsAlgebraic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAlgebraic 📖	mathematical	—	IsAlgebraic	—	—

Algebra.Transcendental

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
transcendental 📖	mathematical	—	Transcendental	—	—

Subalgebra

Definitions

Name	Category	Theorems
IsAlgebraic 📖	MathDef	5 math math: Algebra.isAlgebraic_adjoin_iff, Algebra.isAlgebraic_adjoin_singleton_iff, Algebra.isAlgebraic_iff, isAlgebraic_iff, Algebra.isAlgebraic_adjoin_of_nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAlgebraic_iff 📖	mathematical	—	IsAlgebraic Algebra.IsAlgebraic Subalgebra CommRing.toCommSemiring Ring.toSemiring SetLike.instMembership instSetLike toRing algebra	—	Subtype.forall' Algebra.isAlgebraic_def Subtype.val_injective map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass Polynomial.aeval_algHom_apply val_apply

(root)

Definitions

Name	Category	Theorems
IsAlgebraic 📖	MathDef	57 math math: Algebra.IsAlgebraic.isAlgebraic, Algebraic.cardinalMk_lift_le_mul, IsAlgebraic.of_finite, Subalgebra.mem_algebraicClosure, Algebra.isAlgebraic_adjoin_iff, isAlgebraic_algHom_iff, AlgebraicIndependent.matroid_isBasis_iff, Algebraic.cardinalMk_le_max, IntermediateField.isAlgebraic_iff, Algebra.IsIntegral.isAlgebraic_iff, IntermediateField.isAlgebraic_adjoin_iff, IsAdjoinRoot.isAlgebraic_root, isAlgebraic_rat, Algebra.isAlgebraic_adjoin_singleton_iff, IsIntegral.isAlgebraic, Real.isAlgebraic_tan_rat_mul_pi, Complex.isAlgebraic_sin_rat_mul_pi, Real.isAlgebraic_cos_rat_mul_pi, mem_algebraicClosure_iff, AdjoinRoot.isAlgebraic_root, AlgebraicIndependent.isAlgebraic_adjoin_iff_of_matroid_isBasis, IsTranscendenceBasis.isAlgebraic_iff, IsAlgebraic.of_smul_isIntegral, IntermediateField.isAlgebraic_adjoin_iff_isAlgebraic, Algebraic.cardinalMk_of_countable_of_charZero, Field.isAlgebraic_of_adjoin_eq_adjoin, isAlgebraic_int, Algebra.isAlgebraic_def, IsAlgebraic.iff_exists_smul_integral, IsIntegral.trans_isAlgebraic, Real.isAlgebraic_sin_rat_mul_pi, Subalgebra.isAlgebraic_iff_isAlgebraic_val, isAlgebraic_algebraMap_iff, isAlgebraic_nat, Algebraic.aleph0_le_cardinalMk_of_charZero, isAlgebraic_zero, Algebraic.cardinalMk_le_mul, Algebraic.infinite_of_charZero, IsFractionRing.isAlgebraic_iff, isAlgebraic_ringHom_iff_of_comp_eq, IsAlgebraic.inv_iff, IsAlgebraic.invOf_iff, isAlgebraic_iff_not_injective, Subalgebra.isAlgebraic_bot_iff, isAlgebraic_algebraMap, Complex.isAlgebraic_tan_rat_mul_pi, Algebraic.countable, isAlgebraic_of_mem_rootSet, Algebraic.cardinalMk_of_infinite, Algebra.isAlgebraic_adjoin_of_nonempty, Complex.isAlgebraic_cos_rat_mul_pi, Algebra.IsAlgebraic.isAlgebraic_iff, MvPolynomial.isAlgebraic_of_mem_vars_of_forall_totalDegree_le, isAlgebraic_iff_isIntegral, Algebraic.cardinalMk_lift_of_infinite, isAlgebraic_one, Algebraic.cardinalMk_lift_le_max

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
transcendental_iff 📖	mathematical	—	Transcendental Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instZero	—	Transcendental.eq_1 IsAlgebraic.eq_1

---

← Back to Index