Documentation Verification Report

Field

📁 Source: Mathlib/RingTheory/Adjoin/Field.lean

Statistics

Metric	Count
Definitions `adjoinSingletonEquivAdjoinRootMinpoly`, `liftSingleton`	2
Theorems `adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom`, `coe_adjoinSingletonEquivAdjoinRootMinpoly_symm`, `mem_range_algHom_of_minpoly_splits`, `mem_range_algebraMap_of_minpoly_splits`, `minpoly_splits_tower_top`, `minpoly_splits_tower_top'`, `lift_of_splits`, `adjoin_rank_le`, `minpoly_add_algebraMap_splits`, `minpoly_algebraMap_add_splits`, `minpoly_algebraMap_sub_splits`, `minpoly_neg_splits`, `minpoly_sub_algebraMap_splits`	13
Total	15

AlgEquiv

Definitions

Name	Category	Theorems
`adjoinSingletonEquivAdjoinRootMinpoly` 📖	CompOp	2 math math: `coe_adjoinSingletonEquivAdjoinRootMinpoly_symm`, `adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom` 📖	mathematical	—	`AlgHomClass.toAlgHom` `AdjoinRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `minpoly` `CommRing.toRing` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `AdjoinRoot.instCommRing` `Subalgebra.toSemiring` `AdjoinRoot.instAlgebra` `Algebra.id` `Subalgebra.algebra` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `instFunLike` `AlgEquivClass.toAlgHomClass` `instEquivLike` `instAlgEquivClass` `symm` `adjoinSingletonEquivAdjoinRootMinpoly` `AdjoinRoot.Minpoly.toAdjoin`	—	`AlgEquivClass.toAlgHomClass` `instAlgEquivClass`
`coe_adjoinSingletonEquivAdjoinRootMinpoly_symm` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `AdjoinRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `minpoly` `CommRing.toRing` `Subalgebra` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `AdjoinRoot.instCommRing` `Subalgebra.toSemiring` `AdjoinRoot.instAlgebra` `Algebra.id` `Subalgebra.algebra` `instFunLike` `symm` `adjoinSingletonEquivAdjoinRootMinpoly` `AlgHom` `AlgHom.funLike` `AdjoinRoot.Minpoly.toAdjoin`	—	—

Algebra.adjoin

Definitions

Name	Category	Theorems
`liftSingleton` 📖	CompOp	—

IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_range_algHom_of_minpoly_splits` 📖	mathematical	`IsIntegral` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap` `minpoly`	`Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range`	—	`Set.image_subset_range` `instIsDomain` `Polynomial.Splits.image_rootSet` `DivisionRing.isSimpleRing` `Polynomial.mem_rootSet'` `Polynomial.Monic.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.Monic.map` `minpoly.monic` `minpoly.aeval`
`mem_range_algebraMap_of_minpoly_splits` 📖	mathematical	`IsIntegral` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap` `minpoly`	`Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `Semifield.toCommSemiring`	—	`mem_range_algHom_of_minpoly_splits`
`minpoly_splits_tower_top` 📖	mathematical	`IsIntegral` `CommRing.toRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap` `minpoly`	`Semifield.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`minpoly_splits_tower_top'` `IsScalarTower.algebraMap_eq`
`minpoly_splits_tower_top'` 📖	mathematical	`IsIntegral` `CommRing.toRing` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.comp` `Semiring.toNonAssocSemiring` `algebraMap` `minpoly`	`EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`Polynomial.Splits.of_dvd` `instIsDomain` `Polynomial.map_monic_ne_zero` `minpoly.monic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.map_map` `Polynomial.map_dvd_map'` `minpoly.dvd_map_of_isScalarTower`

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lift_of_splits` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly`	`AlgHom` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `SetLike.coe` `Finset` `Finset.instSetLike` `Subalgebra.toSemiring` `Subalgebra.algebra`	—	`Finset.induction_on` `Finset.coe_empty` `Algebra.adjoin_empty` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Finset.forall_mem_insert` `Finset.coe_insert` `Set.insert_eq` `Set.union_comm` `IsScalarTower.subalgebra'` `IsScalarTower.right` `Algebra.adjoin_union_eq_adjoin_adjoin` `IsIntegral.tower_top` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Splits.of_dvd` `instIsDomain` `map_ne_zero` `DivisionRing.isSimpleRing` `minpoly.ne_zero` `IsScalarTower.algebraMap_eq` `IsScalarTower.of_algHom` `map_map` `Subalgebra.isDomain` `FiniteDimensional.of_subalgebra_toSubmodule` `Submodule.fg_iff_finiteDimensional` `fg_adjoin_of_finite` `Finset.finite_toSet` `map_dvd_map'` `minpoly.dvd_map_of_isScalarTower` `Splits.exists_eval_eq_zero` `degree_map` `LT.lt.ne'` `minpoly.degree_pos` `eval_map`

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_rank_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Module.rank` `Subalgebra` `SetLike.instMembership` `instSetLike` `Algebra.adjoin` `SetLike.coe` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `instModuleSubtypeMem`	—	`rank_toSubmodule` `Module.Free.rank_eq_card_chooseBasisIndex` `adjoin_eq_span_basis` `LE.le.trans` `rank_span_le` `Cardinal.mk_range_le`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`minpoly_add_algebraMap_splits` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`minpoly.add_algebraMap` `Polynomial.map_comp` `Polynomial.map_sub` `Polynomial.map_X` `Polynomial.map_C` `Polynomial.Splits.comp_X_sub_C`
`minpoly_algebraMap_add_splits` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`add_comm` `minpoly_add_algebraMap_splits`
`minpoly_algebraMap_sub_splits` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`neg_sub` `minpoly_neg_splits` `minpoly_sub_algebraMap_splits`
`minpoly_neg_splits` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`minpoly.neg` `Polynomial.map_mul` `Polynomial.Splits.mul` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_neg` `RingHomClass.toAddMonoidHomClass` `map_one` `MonoidHomClass.toOneHomClass` `Polynomial.Splits.C` `Polynomial.map_C` `Polynomial.map_comp` `Polynomial.map_neg` `Polynomial.map_X` `Polynomial.Splits.comp_neg_X`
`minpoly_sub_algebraMap_splits` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`sub_eq_add_neg` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `minpoly_add_algebraMap_splits`

---

← Back to Index