Documentation Verification Report

Polynomial

📁 Source: Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean

Statistics

Metric	Count
Definitions `fiberEquivQuotient`, `residueFieldMapCAlgEquiv`	2
Theorems `exists_mem_span_singleton_map_residueField_eq`, `fiberEquivQuotient_tmul`, `residueFieldMapCAlgEquiv_algebraMap`, `residueFieldMapCAlgEquiv_symm_C`, `residueFieldMapCAlgEquiv_symm_X`	5
Total	7

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mem_span_singleton_map_residueField_eq` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `Polynomial.semiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `span` `ResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Set` `Set.instSingletonSet` `Polynomial.map` `algebraMap` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `Algebra.id` `map` `RingHom` `RingHom.instFunLike` `Polynomial.mapRingHom`	—	`IsPrincipalIdealRing.principal` `EuclideanDomain.to_principal_ideal_domain` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Polynomial.isLocalization` `instIsFractionRingQuotientIdealResidueField` `map_map` `RingHom.algebraMap_toAlgebra` `Polynomial.mapRingHom_comp` `IsScalarTower.algebraMap_eq` `instIsScalarTowerQuotientIdealResidueField` `mem_span_singleton_self` `IsLocalization.mem_map_algebraMap_iff` `mem_map_iff_of_surjective` `Polynomial.map_surjective` `instIsTwoSided_1` `Quotient.mk_surjective` `le_antisymm` `mem_map_of_mem` `IsLocalization.map_units` `Units.eq_mul_inv_iff_mul_eq` `Polynomial.map_map` `mul_mem_right`

Polynomial

Definitions

Name	Category	Theorems
`fiberEquivQuotient` 📖	CompOp	1 math math: `fiberEquivQuotient_tmul`
`residueFieldMapCAlgEquiv` 📖	CompOp	3 math math: `residueFieldMapCAlgEquiv_symm_X`, `residueFieldMapCAlgEquiv_algebraMap`, `residueFieldMapCAlgEquiv_symm_C`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fiberEquivQuotient_tmul` 📖	mathematical	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike`	`AlgEquiv` `Ideal.ResidueField` `Ideal.Fiber` `HasQuotient.Quotient` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Ideal` `Ideal.instHasQuotient_1` `commRing` `IsLocalRing.instCommRingResidueField` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `mapRingHom` `algebraMap` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `RingHom.ker` `RingHom.instRingHomClass` `RingHomClass.toRingHom` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Semifield.toCommSemiring` `Algebra.TensorProduct.instSemiring` `Ideal.Quotient.semiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.to_smulCommClass` `IsLocalRing.ResidueField` `Ideal.instAlgebraQuotient` `AlgEquiv.instFunLike` `fiberEquivQuotient` `TensorProduct.tmul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Ring.toSemiring` `ring` `DivisionRing.toRing` `Field.toDivisionRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `instMul` `C` `map`	—	`RingHom.instRingHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Algebra.to_smulCommClass` `Ideal.instIsTwoSided_1` `AlgHom.liftOfSurjective_apply` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`
`residueFieldMapCAlgEquiv_algebraMap` 📖	mathematical	`Ideal.map` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	`DFunLike.coe` `AlgEquiv` `Ideal.ResidueField` `commRing` `RatFunc` `IsLocalRing.instCommRingResidueField` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Semifield.toCommSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RatFunc.instField` `instIsDomain` `IsLocalRing.ResidueField.instAlgebra` `Localization.AtPrime.instAlgebraOfLiesOver` `algebraOfAlgebra` `Algebra.id` `instIsLocalHomAtPrimeRingHomAlgebraMap` `RatFunc.instAlgebraOfPolynomial` `AlgEquiv.instFunLike` `residueFieldMapCAlgEquiv` `commSemiring` `algebraMap` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `map`	—	`instIsDomain` `instIsLocalHomAtPrimeRingHomAlgebraMap` `Ideal.ResidueField.lift_algebraMap`
`residueFieldMapCAlgEquiv_symm_C` 📖	mathematical	`Ideal.map` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	`DFunLike.coe` `AlgEquiv` `Ideal.ResidueField` `RatFunc` `IsLocalRing.instCommRingResidueField` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `commRing` `Semifield.toCommSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RatFunc.instField` `instIsDomain` `RatFunc.instAlgebraOfPolynomial` `algebraOfAlgebra` `Algebra.id` `IsLocalRing.ResidueField.instAlgebra` `Localization.AtPrime.instAlgebraOfLiesOver` `instIsLocalHomAtPrimeRingHomAlgebraMap` `AlgEquiv.instFunLike` `AlgEquiv.symm` `residueFieldMapCAlgEquiv` `RatFunc.C` `algebraMap`	—	`AlgEquiv.commutes` `instIsDomain` `instIsLocalHomAtPrimeRingHomAlgebraMap`
`residueFieldMapCAlgEquiv_symm_X` 📖	mathematical	`Ideal.map` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	`DFunLike.coe` `AlgEquiv` `Ideal.ResidueField` `RatFunc` `IsLocalRing.instCommRingResidueField` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `commRing` `Semifield.toCommSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RatFunc.instField` `instIsDomain` `RatFunc.instAlgebraOfPolynomial` `algebraOfAlgebra` `Algebra.id` `IsLocalRing.ResidueField.instAlgebra` `Localization.AtPrime.instAlgebraOfLiesOver` `instIsLocalHomAtPrimeRingHomAlgebraMap` `AlgEquiv.instFunLike` `AlgEquiv.symm` `residueFieldMapCAlgEquiv` `RatFunc.X` `commSemiring` `algebraMap` `IsLocalRing.ResidueField.algebra` `OreLocalization.instAlgebra` `X`	—	`AlgEquiv.injective` `instIsDomain` `instIsLocalHomAtPrimeRingHomAlgebraMap` `AlgEquiv.apply_symm_apply` `residueFieldMapCAlgEquiv_algebraMap` `map_X`

---

← Back to Index