Documentation Verification Report

DPMorphism

📁 Source: Mathlib/RingTheory/DividedPowers/DPMorphism.lean

Statistics

Metric	Count
Definitions `DPMorphism`, `coe_ringHom`, `comp`, `fromGens`, `id`, `instFunLike`, `instInhabited`, `mk'`, `toRingHom`, `IsDPMorphism`, `ideal_from_ringHom`	11
Theorems `coe_toRingHom`, `comp_toRingHom`, `dpow_comp`, `ext`, `ext_iff`, `fromGens_coe`, `ideal_comp`, `isDPMorphism`, `toRingHom_apply`, `comp`, `dpow_comp`, `ideal_comp`, `map_dpow`, `of_comp`, `on_span`, `dpow_comp_from_gens`, `dpow_eq_from_gens`, `isDPMorphism_def`, `isDPMorphism_iff`	19
Total	30

DividedPowers

Definitions

Name	Category	Theorems
`DPMorphism` 📖	CompData	2 math math: `DPMorphism.toRingHom_apply`, `DPMorphism.coe_toRingHom`
`IsDPMorphism` 📖	CompData	7 math math: `Quotient.OfSurjective.isDPMorphism`, `IsDPMorphism.on_span`, `isDPMorphism_iff`, `isDPMorphism_def`, `IsSubDPIdeal.isDPMorphism`, `Quotient.isDPMorphism`, `DPMorphism.isDPMorphism`
`ideal_from_ringHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dpow_comp_from_gens` 📖	—	`Ideal.span` `CommSemiring.toSemiring` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `dpow`	—	—	`IsDPMorphism.dpow_comp` `IsDPMorphism.on_span`
`dpow_eq_from_gens` 📖	—	`Ideal.span` `CommSemiring.toSemiring` `dpow`	—	—	`ext` `dpow_comp_from_gens` `Ideal.subset_span` `dpow_null`
`isDPMorphism_def` 📖	mathematical	—	`IsDPMorphism` `Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.map` `RingHom` `RingHom.instFunLike` `dpow` `DFunLike.coe`	—	`IsDPMorphism.ideal_comp` `IsDPMorphism.dpow_comp`
`isDPMorphism_iff` 📖	mathematical	—	`IsDPMorphism` `Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.map` `RingHom` `RingHom.instFunLike` `dpow` `DFunLike.coe`	—	`isDPMorphism_def` `dpow_zero` `Ideal.mem_map_of_mem` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`

DividedPowers.DPMorphism

Definitions

Name	Category	Theorems
`coe_ringHom` 📖	CompOp	—
`comp` 📖	CompOp	1 math math: `comp_toRingHom`
`fromGens` 📖	CompOp	1 math math: `fromGens_coe`
`id` 📖	CompOp	—
`instFunLike` 📖	CompOp	2 math math: `toRingHom_apply`, `coe_toRingHom`
`instInhabited` 📖	CompOp	—
`mk'` 📖	CompOp	—
`toRingHom` 📖	CompOp	8 math math: `dpow_comp`, `comp_toRingHom`, `toRingHom_apply`, `ideal_comp`, `fromGens_coe`, `coe_toRingHom`, `isDPMorphism`, `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toRingHom` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `toRingHom` `DividedPowers.DPMorphism` `instFunLike`	—	—
`comp_toRingHom` 📖	mathematical	—	`toRingHom` `comp` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	—
`dpow_comp` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DividedPowers.dpow` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `toRingHom`	—	—
`ext` 📖	—	`OneHom.toFun` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MonoidHom.toOneHom` `RingHom.toMonoidHom` `toRingHom`	—	—	—
`ext_iff` 📖	mathematical	—	`OneHom.toFun` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MonoidHom.toOneHom` `RingHom.toMonoidHom` `toRingHom`	—	`ext`
`fromGens_coe` 📖	mathematical	`Ideal.span` `CommSemiring.toSemiring` `Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.map` `RingHom` `RingHom.instFunLike` `DFunLike.coe` `DividedPowers.dpow`	`toRingHom` `fromGens`	—	—
`ideal_comp` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.map` `RingHom` `RingHom.instFunLike` `toRingHom`	—	—
`isDPMorphism` 📖	mathematical	—	`DividedPowers.IsDPMorphism` `toRingHom`	—	`ideal_comp` `dpow_comp`
`toRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `toRingHom` `DividedPowers.DPMorphism` `instFunLike`	—	—

DividedPowers.IsDPMorphism

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`DividedPowers.IsDPMorphism`	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`le_trans` `Ideal.map_mono` `ideal_comp` `Ideal.map_map` `dpow_comp` `Ideal.mem_map_of_mem`
`dpow_comp` 📖	mathematical	`DividedPowers.IsDPMorphism` `Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DividedPowers.dpow` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	—	—
`ideal_comp` 📖	mathematical	`DividedPowers.IsDPMorphism`	`Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.map` `RingHom` `RingHom.instFunLike`	—	—
`map_dpow` 📖	mathematical	`DividedPowers.IsDPMorphism` `Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DFunLike.coe` `RingHom` `RingHom.instFunLike` `DividedPowers.dpow`	—	`dpow_comp`
`of_comp` 📖	—	`Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `DividedPowers.IsDPMorphism` `RingHom.comp`	—	—	`on_span` `RingHom.comp_apply` `ideal_comp` `Ideal.mem_map_of_mem` `dpow_comp`
`on_span` 📖	mathematical	`Ideal.span` `CommSemiring.toSemiring` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `DividedPowers.dpow`	`DividedPowers.IsDPMorphism`	—	`Ideal.map_span` `RingHom.instRingHomClass` `Ideal.span_le` `DividedPowers.DPMorphism.fromGens_coe` `DividedPowers.DPMorphism.dpow_comp`

---

← Back to Index