Documentation Verification Report

Quotient

📁 Source: Mathlib/RingTheory/Polynomial/Quotient.lean

Statistics

Metric	Count
Definitions `polynomialQuotientEquivQuotientPolynomial`, `quotientEquivQuotientMvPolynomial`, `quotientSpanCXSubCAlgEquiv`, `quotientSpanCXSubCXSubCAlgEquiv`, `quotientSpanXSubCAlgEquiv`	5
Theorems `of_isPrincipalIdealRing_polynomial`, `eq_zero_of_polynomial_mem_map_range`, `eval₂_C_mk_eq_zero`, `isDomain_map_C_quotient`, `polynomialQuotientEquivQuotientPolynomial_map_mk`, `polynomialQuotientEquivQuotientPolynomial_symm_mk`, `quotient_map_C_eq_zero`, `eval₂_C_mk_eq_zero`, `quotientEquivQuotientMvPolynomial_leftInverse`, `quotientEquivQuotientMvPolynomial_rightInverse`, `quotient_map_C_eq_zero`, `modByMonic_eq_zero_iff_quotient_eq_zero`, `quotientSpanXSubCAlgEquiv_mk`, `quotientSpanXSubCAlgEquiv_symm_apply`	14
Total	19

Ideal

Definitions

Name	Category	Theorems
`polynomialQuotientEquivQuotientPolynomial` 📖	CompOp	2 math math: `polynomialQuotientEquivQuotientPolynomial_symm_mk`, `polynomialQuotientEquivQuotientPolynomial_map_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_of_polynomial_mem_map_range` 📖	mathematical	`Polynomial` `HasQuotient.Quotient` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `Ring.toSemiring` `Polynomial.ring` `CommRing.toRing` `instHasQuotient` `Subring` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Quotient.commRing` `Polynomial.commRing` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `RingHom.comp` `Semiring.toNonAssocSemiring` `Quotient.ring` `instIsTwoSided_1` `Polynomial.C` `SubsemiringClass.toCommSemiring` `Quotient.commSemiring` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `Polynomial.semiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `map` `RingHom` `RingHom.instFunLike` `Polynomial.mapRingHom` `RingHom.rangeRestrict` `DFunLike.coe`	`HasQuotient.Quotient` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `Ring.toSemiring` `Polynomial.ring` `CommRing.toRing` `instHasQuotient` `Subring` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Quotient.commRing` `Polynomial.commRing` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `RingHom.comp` `Semiring.toNonAssocSemiring` `Quotient.ring` `instIsTwoSided_1` `Polynomial.C` `ZeroMemClass.zero` `Submodule.Quotient.instZeroQuotient` `Ring.toAddCommGroup` `Semiring.toModule` `Polynomial.semiring` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Quotient.instRingQuotient` `SubsemiringClass.toAddSubmonoidClass` `Quotient.semiring` `SubringClass.toSubsemiringClass` `Subring.instSubringClass`	—	`instIsTwoSided_1` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `RingHom.instRingHomClass` `polynomial_mem_ideal_of_coeff_mem_ideal` `mem_comap` `Quotient.eq_zero_iff_mem` `RingHom.comp_apply` `Polynomial.coe_mapRingHom` `RingHom.mem_ker` `RingHom.coe_rangeRestrict` `Polynomial.coeff_map` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `RingHom.mem_range` `mem_image_of_mem_map_of_surjective` `Polynomial.map_surjective` `RingHom.rangeRestrict_surjective` `add_mem` `map_sub` `RingHomClass.toAddMonoidHomClass` `sub_eq_zero` `Polynomial.map_C` `sub_add_cancel`
`eval₂_C_mk_eq_zero` 📖	mathematical	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `Polynomial.semiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `map` `RingHom` `RingHom.instFunLike` `Polynomial.C`	`DFunLike.coe` `RingHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `instHasQuotient` `Quotient.semiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Polynomial.commSemiring` `Quotient.commSemiring` `RingHom.instFunLike` `Polynomial.eval₂RingHom` `RingHom.comp` `Polynomial.C` `instIsTwoSided_1` `Polynomial.X` `Polynomial.instZero`	—	`instIsTwoSided_1` `Polynomial.sum_monomial_eq` `Polynomial.eval₂_sum` `Finset.sum_eq_zero` `Polynomial.eval₂_monomial` `mul_eq_zero_of_left` `Polynomial.ext` `RingHom.comp_apply` `Polynomial.coeff_C` `Quotient.eq_zero_iff_mem` `mem_map_C_iff`
`isDomain_map_C_quotient` 📖	mathematical	—	`IsDomain` `HasQuotient.Quotient` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `Polynomial.semiring` `instHasQuotient_1` `Polynomial.commRing` `map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `Quotient.semiring`	—	`MulEquiv.isDomain` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `Quotient.isDomain` `instIsTwoSided_1` `RingEquivClass.toMulEquivClass` `RingEquiv.instRingEquivClass`
`polynomialQuotientEquivQuotientPolynomial_map_mk` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Polynomial` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instHasQuotient_1` `Quotient.semiring` `Polynomial.semiring` `Polynomial.commRing` `map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `Polynomial.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Quotient.commRing` `Polynomial.instAdd` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `polynomialQuotientEquivQuotientPolynomial` `Polynomial.map` `CommRing.toRing` `instIsTwoSided_1` `Ring.toSemiring` `Polynomial.ring` `instHasQuotient` `Quotient.ring`	—	`RingEquiv.injective` `instIsTwoSided_1` `RingEquiv.symm_apply_apply`
`polynomialQuotientEquivQuotientPolynomial_symm_mk` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `HasQuotient.Quotient` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `Polynomial.semiring` `instHasQuotient_1` `Polynomial.commRing` `map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `Quotient.semiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Quotient.commRing` `Polynomial.instMul` `Distrib.toAdd` `Polynomial.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `polynomialQuotientEquivQuotientPolynomial` `Ring.toSemiring` `Polynomial.ring` `CommRing.toRing` `instHasQuotient` `Quotient.ring` `instIsTwoSided_1` `Polynomial.map`	—	`instIsTwoSided_1` `quotient_map_C_eq_zero` `eval₂_C_mk_eq_zero` `polynomialQuotientEquivQuotientPolynomial.eq_1` `Equiv.left_inv` `Equiv.right_inv` `RingEquiv.map_mul'` `RingEquiv.map_add'` `Polynomial.coe_eval₂RingHom` `Polynomial.eval₂_eq_eval_map` `Polynomial.map_map` `Polynomial.eval₂_C_X`
`quotient_map_C_eq_zero` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `Ring.toSemiring` `Polynomial.ring` `CommRing.toRing` `instHasQuotient` `map` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `Quotient.ring` `instIsTwoSided_1` `Polynomial.commRing` `RingHom.comp` `Submodule.Quotient.instZeroQuotient` `Ring.toAddCommGroup` `Semiring.toModule`	—	`instIsTwoSided_1` `RingHom.comp_apply` `Quotient.eq_zero_iff_mem` `mem_map_of_mem`

Ideal.IsField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_isPrincipalIdealRing_polynomial` 📖	mathematical	—	`IsField` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`MulEquiv.isField` `Ideal.Quotient.maximal_ideal_iff_isField_quotient` `PrincipalIdealRing.isMaximal_of_irreducible` `Polynomial.irreducible_X_sub_C`

MvPolynomial

Definitions

Name	Category	Theorems
`quotientEquivQuotientMvPolynomial` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eval₂_C_mk_eq_zero` 📖	mathematical	`MvPolynomial` `CommRing.toCommSemiring` `Ideal` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.map` `RingHom` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `RingHom.instFunLike` `C`	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.commSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra.commSemiring` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `RingHom.instFunLike` `eval₂Hom` `RingHom.comp` `C` `Ideal.instIsTwoSided_1` `X` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Finsupp.instAdd`	—	`Ideal.instIsTwoSided_1` `as_sum` `coe_eval₂Hom` `eval₂_sum` `Finset.sum_eq_zero` `eval₂_monomial` `mul_eq_zero_of_left` `mem_map_C_iff` `RingHom.instRingHomClass` `RingHom.mem_ker` `Ideal.mk_ker` `C_0`
`quotientEquivQuotientMvPolynomial_leftInverse` 📖	mathematical	—	`HasQuotient.Quotient` `MvPolynomial` `CommRing.toCommSemiring` `Ideal` `Ring.toSemiring` `AddMonoidAlgebra.ring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Ideal.instHasQuotient` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidAlgebra.semiring` `RingHom.instFunLike` `C` `Ideal.Quotient.commSemiring` `eval₂` `AddMonoidAlgebra.commRing` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `Ideal.Quotient.lift` `Ideal.instIsTwoSided_1` `RingHom.comp` `Ideal.Quotient.ring` `quotient_map_C_eq_zero` `DFunLike.coe` `X` `AddMonoidAlgebra.commSemiring` `eval₂Hom` `eval₂_C_mk_eq_zero`	—	`Ideal.instIsTwoSided_1` `quotient_map_C_eq_zero` `eval₂_C_mk_eq_zero` `Ideal.Quotient.mk_surjective` `induction_on` `eval₂Hom_C` `RingHom.comp_apply` `eval₂_C` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `eval₂_add` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `eval₂_X` `eval₂_mul`
`quotientEquivQuotientMvPolynomial_rightInverse` 📖	mathematical	—	`HasQuotient.Quotient` `MvPolynomial` `CommRing.toCommSemiring` `Ideal` `Ring.toSemiring` `AddMonoidAlgebra.ring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Ideal.instHasQuotient` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidAlgebra.semiring` `RingHom.instFunLike` `C` `Ideal.Quotient.commSemiring` `eval₂` `AddMonoidAlgebra.commRing` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `Ideal.Quotient.lift` `Ideal.instIsTwoSided_1` `RingHom.comp` `Ideal.Quotient.ring` `quotient_map_C_eq_zero` `DFunLike.coe` `X` `AddMonoidAlgebra.commSemiring` `eval₂Hom` `eval₂_C_mk_eq_zero`	—	`induction_on` `Ideal.instIsTwoSided_1` `eval₂_C_mk_eq_zero` `quotient_map_C_eq_zero` `Ideal.Quotient.mk_surjective` `eval₂_C` `eval₂Hom_C` `eval₂_add` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `eval₂_mul` `eval₂_X` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`
`quotient_map_C_eq_zero` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `MvPolynomial` `CommRing.toCommSemiring` `Ideal` `Ring.toSemiring` `AddMonoidAlgebra.ring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Ideal.instHasQuotient` `Ideal.map` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidAlgebra.semiring` `RingHom.instFunLike` `C` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `AddMonoidAlgebra.commRing` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `RingHom.comp` `Submodule.Quotient.instZeroQuotient` `AddMonoidAlgebra.addAddCommGroup` `Semiring.toModule`	—	`Ideal.instIsTwoSided_1` `Ideal.mem_map_of_mem`

Polynomial

Definitions

Name	Category	Theorems
`quotientSpanCXSubCAlgEquiv` 📖	CompOp	—
`quotientSpanCXSubCXSubCAlgEquiv` 📖	CompOp	—
`quotientSpanXSubCAlgEquiv` 📖	CompOp	2 math math: `quotientSpanXSubCAlgEquiv_symm_apply`, `quotientSpanXSubCAlgEquiv_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`modByMonic_eq_zero_iff_quotient_eq_zero` 📖	mathematical	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`modByMonic` `CommRing.toRing` `Polynomial` `Ring.toSemiring` `instZero` `DFunLike.coe` `RingHom` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `HasQuotient.Quotient` `Ideal` `ring` `Ideal.instHasQuotient` `Ideal.span` `semiring` `Set` `Set.instSingletonSet` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `commRing` `RingHom.instFunLike` `Submodule.Quotient.instZeroQuotient` `Ring.toAddCommGroup` `Semiring.toModule`	—	`Ideal.instIsTwoSided_1` `modByMonic_eq_zero_iff_dvd` `Ideal.Quotient.eq_zero_iff_dvd`
`quotientSpanXSubCAlgEquiv_mk` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `HasQuotient.Quotient` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `semiring` `Ideal.instHasQuotient_1` `commRing` `Ideal.span` `Set` `Set.instSingletonSet` `instSub` `CommRing.toRing` `X` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient` `algebraOfAlgebra` `Algebra.id` `AlgEquiv.instFunLike` `quotientSpanXSubCAlgEquiv` `Ring.toSemiring` `ring` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `eval`	—	`Ideal.instIsTwoSided_1`
`quotientSpanXSubCAlgEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `HasQuotient.Quotient` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `semiring` `Ideal.instHasQuotient_1` `commRing` `Ideal.span` `Set` `Set.instSingletonSet` `instSub` `CommRing.toRing` `X` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C` `Ideal.Quotient.semiring` `Algebra.id` `Ideal.instAlgebraQuotient` `algebraOfAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `quotientSpanXSubCAlgEquiv` `algebraMap`	—	—

---

← Back to Index