Documentation Verification Report

Quotient

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

Statistics

Metric	Count
Definitions `onQuot`, `onQuotVal`, `onQuot`, `onQuotVal`	4
Theorems `comap_onQuot_eq`, `comap_supp`, `onQuot_comap_eq`, `self_le_supp_comap`, `supp_quot`, `supp_quot_supp`, `comap_onQuot_eq`, `onQuot_comap_eq`, `self_le_supp_comap`, `supp_quot`, `supp_quot_supp`	11
Total	15

AddValuation

Definitions

Name	Category	Theorems
`onQuot` 📖	CompOp	3 math math: `onQuot_comap_eq`, `comap_onQuot_eq`, `supp_quot`
`onQuotVal` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_onQuot_eq` 📖	mathematical	—	`onQuot` `comap` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.instRingQuotient` `Ideal.instIsTwoSided_1` `self_le_supp_comap`	—	`Valuation.comap_onQuot_eq`
`comap_supp` 📖	mathematical	—	`supp` `comap` `CommRing.toRing` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass`	—	`Valuation.comap_supp`
`onQuot_comap_eq` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `supp`	`comap` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.instRingQuotient` `Ideal.instIsTwoSided_1` `onQuot`	—	`Valuation.onQuot_comap_eq`
`self_le_supp_comap` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `supp` `comap` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.instRingQuotient` `Ideal.instIsTwoSided_1`	—	`Valuation.self_le_supp_comap`
`supp_quot` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `supp`	`HasQuotient.Quotient` `Ideal.instHasQuotient_1` `Ideal.Quotient.commRing` `onQuot` `Ideal.map` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `RingHom` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Ideal.Quotient.semiring` `RingHom.instFunLike`	—	`Valuation.supp_quot`
`supp_quot_supp` 📖	mathematical	—	`supp` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Valuation.supp` `Multiplicative` `OrderDual` `instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual` `Ideal.Quotient.commRing` `Valuation.onQuot` `le_rfl` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.pointwiseZero`	—	`Valuation.supp_quot_supp`

Valuation

Definitions

Name	Category	Theorems
`onQuot` 📖	CompOp	5 math math: `supp_quot_supp`, `comap_onQuot_eq`, `supp_quot`, `onQuot_comap_eq`, `AddValuation.supp_quot_supp`
`onQuotVal` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_onQuot_eq` 📖	mathematical	—	`onQuot` `comap` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.instRingQuotient` `Ideal.instIsTwoSided_1` `self_le_supp_comap`	—	`ext` `Ideal.instIsTwoSided_1` `self_le_supp_comap`
`onQuot_comap_eq` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `supp`	`comap` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.instRingQuotient` `Ideal.instIsTwoSided_1` `onQuot`	—	`ext` `Ideal.instIsTwoSided_1`
`self_le_supp_comap` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `supp` `comap` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.instRingQuotient` `Ideal.instIsTwoSided_1`	—	`Ideal.instIsTwoSided_1` `RingHom.instRingHomClass` `comap_supp` `Ideal.map_le_iff_le_comap` `Ideal.map_quotient_self`
`supp_quot` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `supp`	`HasQuotient.Quotient` `Ideal.instHasQuotient_1` `Ideal.Quotient.commRing` `onQuot` `Ideal.map` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `RingHom` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Ideal.Quotient.semiring` `RingHom.instFunLike`	—	`le_antisymm` `Ideal.instIsTwoSided_1` `Ideal.subset_span` `RingHom.instRingHomClass` `Ideal.map_le_iff_le_comap`
`supp_quot_supp` 📖	mathematical	—	`supp` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.Quotient.commRing` `onQuot` `le_rfl` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.pointwiseZero`	—	`le_rfl` `Ideal.instIsTwoSided_1` `supp_quot` `Ideal.map_quotient_self`

---

← Back to Index