Documentation Verification Report

Adjoin

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

Statistics

Metric	Count
Definitions `aevalEquivField`, `reprField`	2
Theorems `aevalEquivField_algebraMap_apply_coe`, `aevalEquivField_apply_coe`, `liftAlgHom_comp_reprField`, `lift_reprField`	4
Total	6

AlgebraicIndependent

Definitions

Name	Category	Theorems
`aevalEquivField` 📖	CompOp	2 math math: `aevalEquivField_apply_coe`, `aevalEquivField_algebraMap_apply_coe`
`reprField` 📖	CompOp	2 math math: `lift_reprField`, `liftAlgHom_comp_reprField`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aevalEquivField_algebraMap_apply_coe` 📖	mathematical	`AlgebraicIndependent` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set.range` `DFunLike.coe` `AlgEquiv` `FractionRing` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `MvPolynomial.instCommRingMvPolynomial` `OreLocalization.instSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommRing.toCommSemiring` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `IntermediateField.toField` `OreLocalization.instAlgebra` `MvPolynomial.algebra` `Algebra.id` `IntermediateField.algebra'` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule` `AlgEquiv.instFunLike` `aevalEquivField` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `AlgHom` `AlgHom.funLike` `MvPolynomial.aeval`	—	`IsScalarTower.left` `IsFractionRing.lift_algebraMap` `MvPolynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `instIsDomain` `Localization.isLocalization` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `algebraicIndependent_iff_injective_aeval`
`aevalEquivField_apply_coe` 📖	mathematical	`AlgebraicIndependent` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set.range` `DFunLike.coe` `AlgEquiv` `FractionRing` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `MvPolynomial.instCommRingMvPolynomial` `OreLocalization.instSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommRing.toCommSemiring` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `IntermediateField.toField` `OreLocalization.instAlgebra` `MvPolynomial.algebra` `Algebra.id` `IntermediateField.algebra'` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule` `AlgEquiv.instFunLike` `aevalEquivField` `RingHom` `Semiring.toNonAssocSemiring` `FractionRing.field` `MvPolynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instIsDomain` `RingHom.instFunLike` `IsFractionRing.lift` `Localization.isLocalization` `AlgHom.toRingHom` `Field.toCommRing` `MvPolynomial.aeval` `AlgHom` `AlgHom.funLike` `algebraicIndependent_iff_injective_aeval`	—	`IsScalarTower.left`
`liftAlgHom_comp_reprField` 📖	mathematical	`AlgebraicIndependent` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`AlgHom.comp` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set.range` `FractionRing` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `MvPolynomial.instCommRingMvPolynomial` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `IntermediateField.toField` `FractionRing.field` `MvPolynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instIsDomain` `IntermediateField.algebra'` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule` `OreLocalization.instAlgebra` `MvPolynomial.commSemiring` `nonZeroDivisors` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `MvPolynomial.algebra` `IsFractionRing.liftAlgHom` `Localization.isLocalization` `OreLocalization.instIsScalarTower` `CommMonoid.toMonoid` `Monoid.toMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsScalarTower.right` `MvPolynomial.aeval` `Field.toCommRing` `DFunLike.coe` `AlgHom` `AlgHom.funLike` `algebraicIndependent_iff_injective_aeval` `reprField` `IntermediateField.val`	—	`AlgHom.ext` `IsScalarTower.left` `MvPolynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `instIsDomain` `Localization.isLocalization` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `algebraicIndependent_iff_injective_aeval` `lift_reprField`
`lift_reprField` 📖	mathematical	`AlgebraicIndependent` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`DFunLike.coe` `RingHom` `FractionRing` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `MvPolynomial.instCommRingMvPolynomial` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `FractionRing.field` `MvPolynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instIsDomain` `RingHom.instFunLike` `IsFractionRing.lift` `CommRing.toCommSemiring` `OreLocalization.instAlgebra` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `Algebra.id` `Localization.isLocalization` `AlgHom.toRingHom` `Field.toCommRing` `MvPolynomial.algebra` `MvPolynomial.aeval` `AlgHom` `AlgHom.funLike` `algebraicIndependent_iff_injective_aeval` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set.range` `IntermediateField.toField` `OreLocalization.instSemiring` `IntermediateField.algebra'` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule` `reprField`	—	`IsScalarTower.left` `AlgEquiv.apply_symm_apply`

---

← Back to Index