Documentation Verification Report

AlgebraicClosure

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

Statistics

Metric	Count
Definitions	0
Theorems `algebraicIndependent_iff`, `isTranscendenceBasis_iff`, `algebraicIndependent_iff`, `isTranscendenceBasis_iff`, `algebraicClosure`, `extendScalars`, `extendScalars_of_isIntegral`, `integralClosure`, `subalgebraAlgebraicClosure`, `algebraicIndependent_adjoin_iff`, `isAlgebraic_adjoin_iff`, `isAlgebraic_adjoin_iff_bot`, `isAlgebraic_adjoin_iff_top`, `isTranscendenceBasis_adjoin_iff`, `transcendental_adjoin_iff`	15
Total	15

Algebra.IsAlgebraic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraicIndependent_iff` 📖	mathematical	—	`AlgebraicIndependent`	—	`AlgebraicIndependent.extendScalars` `AlgebraicIndependent.restrictScalars` `FaithfulSMul.algebraMap_injective`
`isTranscendenceBasis_iff` 📖	mathematical	—	`IsTranscendenceBasis`	—	`algebraicIndependent_iff`

Algebra.IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraicIndependent_iff` 📖	mathematical	—	`AlgebraicIndependent`	—	`AlgebraicIndependent.extendScalars_of_isIntegral` `AlgebraicIndependent.restrictScalars` `FaithfulSMul.algebraMap_injective`
`isTranscendenceBasis_iff` 📖	mathematical	—	`IsTranscendenceBasis`	—	`algebraicIndependent_iff`

AlgebraicIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraicClosure` 📖	mathematical	`AlgebraicIndependent` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `algebraicClosure` `IntermediateField.toField` `IntermediateField.instAlgebraSubtypeMem` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Algebra.id` `Semifield.toCommSemiring` `Field.toSemifield`	—	`extendScalars` `IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `SubsemiringClass.noZeroDivisors` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsDomain.to_noZeroDivisors` `instIsDomain` `algebraicClosure.isAlgebraic`
`extendScalars` 📖	—	`AlgebraicIndependent`	—	—	`algebraicIndependent_of_finite_type'` `Algebra.IsAlgebraic.injective_tower_top` `algebraMap_injective` `Algebra.adjoin_le` `Algebra.subset_adjoin` `IsScalarTower.of_algebraMap_eq` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.instSubsemiringClass` `Function.Injective.noZeroDivisors` `Set.image_eq_range` `AlgEquiv.injective` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `MvPolynomial.instNoZeroDivisors` `Subalgebra.inclusion_injective` `RingHom.instRingHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `isAlgebraic_algHom_iff` `Subtype.val_injective` `Algebra.IsAlgebraic.nontrivial` `Function.Injective.nontrivial` `Algebra.adjoin_induction` `isAlgebraic_algebraMap` `SubsemiringClass.nontrivial` `IsAlgebraic.extendScalars` `IsScalarTower.subalgebra'` `IsScalarTower.right` `IsAlgebraic.algHom` `Algebra.IsAlgebraic.isAlgebraic` `IsAlgebraic.add` `IsAlgebraic.mul` `Transcendental.extendScalars` `transcendental_adjoin`
`extendScalars_of_isIntegral` 📖	—	`AlgebraicIndependent`	—	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Module.nontrivial` `extendScalars` `Algebra.IsIntegral.isAlgebraic`
`integralClosure` 📖	mathematical	`AlgebraicIndependent`	`Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `integralClosure` `Subalgebra.toCommRing` `Subalgebra.toAlgebra` `Algebra.id`	—	`extendScalars_of_isIntegral` `IsScalarTower.subalgebra'` `IsScalarTower.right` `Subalgebra.noZeroDivisors` `integralClosure.AlgebraIsIntegral`
`subalgebraAlgebraicClosure` 📖	mathematical	`AlgebraicIndependent`	`Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Subalgebra.algebraicClosure` `Subalgebra.toCommRing` `Subalgebra.toAlgebra` `Algebra.id`	—	`extendScalars` `IsScalarTower.subalgebra'` `IsScalarTower.right` `Subalgebra.noZeroDivisors` `instIsAlgebraicSubtypeMemSubalgebraAlgebraicClosure`

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraicIndependent_adjoin_iff` 📖	mathematical	—	`AlgebraicIndependent` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `instAlgebraSubtypeMem` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Subalgebra` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subalgebra.instSetLike` `Algebra.adjoin` `Subalgebra.toCommRing` `Subalgebra.toAlgebra`	—	`Algebra.IsAlgebraic.algebraicIndependent_iff` `algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1` `SubsemiringClass.noZeroDivisors` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `IsDomain.to_noZeroDivisors` `instIsDomain` `algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin` `algebraAdjoinAdjoin.instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin`
`isAlgebraic_adjoin_iff` 📖	mathematical	—	`IsAlgebraic` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `instAlgebraSubtypeMem` `Ring.toSemiring` `Subalgebra` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subalgebra.instSetLike` `Algebra.adjoin` `Subalgebra.toCommRing` `Subalgebra.toAlgebra`	—	`Algebra.IsAlgebraic.isAlgebraic_iff` `algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1` `SubsemiringClass.noZeroDivisors` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `IsDomain.to_noZeroDivisors` `instIsDomain` `algebraAdjoinAdjoin.instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin` `algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin`
`isAlgebraic_adjoin_iff_bot` 📖	mathematical	—	`Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `DivisionRing.toRing` `Field.toDivisionRing` `toField` `algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Subalgebra` `Semifield.toCommSemiring` `Subalgebra.instSetLike` `Algebra.adjoin` `Subalgebra.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Subalgebra.algebra'`	—	`Algebra.IsAlgebraic.isAlgebraic_iff_bot` `algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin` `Subalgebra.noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `algebraAdjoinAdjoin.instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin` `algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin`
`isAlgebraic_adjoin_iff_top` 📖	mathematical	—	`Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `instAlgebraSubtypeMem` `Ring.toSemiring` `Subalgebra` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subalgebra.instSetLike` `Algebra.adjoin` `Subalgebra.toCommRing` `Subalgebra.toAlgebra`	—	`Algebra.IsAlgebraic.isAlgebraic_iff_top` `algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1` `SubsemiringClass.noZeroDivisors` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `IsDomain.to_noZeroDivisors` `instIsDomain` `algebraAdjoinAdjoin.instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin` `algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin`
`isTranscendenceBasis_adjoin_iff` 📖	mathematical	—	`IsTranscendenceBasis` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `instAlgebraSubtypeMem` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Subalgebra` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subalgebra.instSetLike` `Algebra.adjoin` `Subalgebra.toCommRing` `Subalgebra.toAlgebra`	—	`Algebra.IsAlgebraic.isTranscendenceBasis_iff` `algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1` `SubsemiringClass.noZeroDivisors` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `IsDomain.to_noZeroDivisors` `instIsDomain` `algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin` `algebraAdjoinAdjoin.instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin`
`transcendental_adjoin_iff` 📖	mathematical	—	`Transcendental` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `instAlgebraSubtypeMem` `Ring.toSemiring` `Subalgebra` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subalgebra.instSetLike` `Algebra.adjoin` `Subalgebra.toCommRing` `Subalgebra.toAlgebra`	—	`Algebra.IsAlgebraic.transcendental_iff` `algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1` `SubsemiringClass.noZeroDivisors` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `IsDomain.to_noZeroDivisors` `instIsDomain` `algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin` `algebraAdjoinAdjoin.instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin`

---

← Back to Index