Documentation Verification Report

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	80 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`, `IntermediateField.isAlgebraic_iSup`, `AlgebraicClosure.isAlgebraic`, `instIsAlgebraicMvPolynomialOfNoZeroDivisors_1`, `IsAlgebraic.isAlgebraic_iff_top`, `RatFunc.isAlgebraic_adjoin_simple_X'`, `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	6 math math: `Algebra.isAlgebraic_adjoin_iff`, `Algebra.isAlgebraic_adjoin_singleton_iff`, `Algebra.isAlgebraic_iff`, `isAlgebraic_solvableByRad`, `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	87 math math: `IsAlgebraic.adjoin_singleton`, `Algebra.IsAlgebraic.isAlgebraic`, `Algebraic.cardinalMk_lift_le_mul`, `IsAlgebraic.of_finite`, `IsAlgebraic.sub`, `Subalgebra.mem_algebraicClosure`, `Algebra.isAlgebraic_adjoin_iff`, `IsAlgebraic.invOf`, `isAlgebraic_algHom_iff`, `IsAlgebraic.restrictScalars`, `AlgebraicIndependent.matroid_isBasis_iff`, `IsAlgebraic.zsmul`, `IsAlgebraic.algHom`, `Algebraic.cardinalMk_le_max`, `IntermediateField.isAlgebraic_iff`, `IsAlgebraic.nsmul`, `Algebra.IsIntegral.isAlgebraic_iff`, `IntermediateField.isAlgebraic_adjoin_iff`, `RatFunc.IntermediateField.isAlgebraic_X`, `IsAdjoinRoot.isAlgebraic_root`, `IsAlgebraic.inv`, `isAlgebraic_rat`, `IsAlgebraic.tower_top`, `Algebra.isAlgebraic_adjoin_singleton_iff`, `IsAlgebraic.smul`, `IsAlgebraic.tower_top_of_subalgebra_le`, `IsIntegral.isAlgebraic`, `Real.isAlgebraic_tan_rat_mul_pi`, `Complex.isAlgebraic_sin_rat_mul_pi`, `IsAlgebraic.extendScalars`, `Real.isAlgebraic_cos_rat_mul_pi`, `mem_algebraicClosure_iff`, `IsAlgebraic.add`, `IsAlgebraic.of_aeval`, `IsAlgebraic.restrictScalars_of_isIntegral`, `AdjoinRoot.isAlgebraic_root`, `AlgebraicIndependent.isAlgebraic_adjoin_iff_of_matroid_isBasis`, `IsTranscendenceBasis.isAlgebraic_iff`, `IsAlgebraic.of_pow`, `IsAlgebraic.of_smul_isIntegral`, `IntermediateField.isAlgebraic_adjoin_iff_isAlgebraic`, `Algebraic.cardinalMk_of_countable_of_charZero`, `Field.isAlgebraic_of_adjoin_eq_adjoin`, `IsAlgebraic.adjoin_of_forall_isAlgebraic`, `isAlgebraic_int`, `Algebra.isAlgebraic_def`, `IsAlgebraic.iff_exists_smul_integral`, `IsIntegral.trans_isAlgebraic`, `IsAlgebraic.pow`, `Real.isAlgebraic_sin_rat_mul_pi`, `IsAlgebraic.ringHom_of_comp_eq`, `Subalgebra.isAlgebraic_iff_isAlgebraic_val`, `isAlgebraic_algebraMap_iff`, `IsAlgebraic.of_smul`, `isAlgebraic_nat`, `Algebraic.aleph0_le_cardinalMk_of_charZero`, `IsAlgebraic.of_aeval_of_transcendental`, `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.tmul`, `isAlgebraic_iff_not_injective`, `IsAlgebraic.neg`, `Subalgebra.isAlgebraic_bot_iff`, `isAlgebraic_algebraMap`, `Complex.isAlgebraic_tan_rat_mul_pi`, `IsAlgebraic.mul`, `IsAlgebraic.of_mul`, `IsAlgebraic.algebraMap`, `Algebraic.countable`, `isAlgebraic_of_mem_rootSet`, `IsAlgebraic.of_ringHom_of_comp_eq`, `Subalgebra.isAlgebraic_of_isAlgebraic_bot`, `Algebraic.cardinalMk_of_infinite`, `Algebra.isAlgebraic_adjoin_of_nonempty`, `Complex.isAlgebraic_cos_rat_mul_pi`, `Algebra.IsAlgebraic.isAlgebraic_iff`, `RatFunc.isAlgebraic_adjoin_simple_X`, `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