Documentation Verification Report

Basic

📁 Source: Mathlib/RingTheory/LocalRing/RingHom/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `isLocalHom`, `of_surjective`, `instIsLocalHomRingHomOfNontrivial`, `local_hom_TFAE`, `of_surjective`, `surjective_units_map_of_local_ringHom`, `isLocalRing`, `domain_isLocalRing`, `isLocalHom_comp`, `instIsLocalHomZModRingHomOfIsLocalRingOfNontrivial`, `isLocalHom_id`, `isLocalHom_of_comp`, `isLocalHom_toRingHom`, `map_nonunit`	14
Total	14

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalHom` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	`IsLocalHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`IsLocalHom.of_surjective`

IsLocalHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	`IsLocalHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`IsLocalRing.of_surjective'` `RingHom.instRingHomClass` `List.TFAE.out` `IsLocalRing.local_hom_TFAE` `Ideal.comap_isMaximal_of_surjective` `IsLocalRing.maximalIdeal.isMaximal` `Eq.le` `ExistsUnique.unique` `IsLocalRing.maximal_ideal_unique`

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsLocalHomRingHomOfNontrivial` 📖	mathematical	—	`IsLocalHom` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `RingHom.instFunLike`	—	`RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsUnit.ne_zero`
`local_hom_TFAE` 📖	mathematical	—	`List.TFAE` `IsLocalHom` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `RingHom.instFunLike` `Set` `Set.instHasSubset` `Set.image` `DFunLike.coe` `SetLike.coe` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `maximalIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Ideal.map` `Ideal.comap` `RingHom.instRingHomClass`	—	`map_nonunit` `RingHom.instRingHomClass` `Set.image_subset_iff` `Ideal.map_le_iff_le_comap` `not_imp_not` `Ideal.ext` `not_iff_not` `isUnit_map_iff` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `le_of_eq` `List.tfae_of_cycle`
`of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike`	`IsLocalRing`	—	`of_isUnit_or_isUnit_of_isUnit_add` `RingHom.isUnit_map` `isUnit_or_isUnit_of_isUnit_add` `IsLocalHom.map_nonunit` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`surjective_units_map_of_local_ringHom` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	`Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidHom` `MulOneClass.toMulOne` `Units.instMulOneClass` `MonoidHom.instFunLike` `Units.map` `RingHom.toMonoidHom`	—	`isUnit_of_map_unit` `Units.isUnit` `Units.ext`

RingEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalRing` 📖	mathematical	—	`IsLocalRing`	—	`IsLocalRing.of_surjective` `Equiv.nontrivial` `IsLocalRing.toNontrivial` `RingEquivClass.toRingHomClass` `instRingEquivClass` `isLocalHom_toRingHom` `isLocalHom_equiv` `RingEquivClass.toMulEquivClass` `surjective`

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`domain_isLocalRing` 📖	mathematical	—	`IsLocalRing`	—	`IsLocalRing.of_nonunits_add` `domain_nontrivial` `IsLocalRing.toNontrivial` `map_mem_nonunits_iff` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `instRingHomClass` `map_add` `IsLocalRing.nonunits_add`
`isLocalHom_comp` 📖	mathematical	—	`IsLocalHom` `RingHom` `Semiring.toNonAssocSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instFunLike` `comp`	—	`IsLocalHom.map_nonunit`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsLocalHomZModRingHomOfIsLocalRingOfNontrivial` 📖	mathematical	—	`IsLocalHom` `ZMod` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `RingHom.instFunLike`	—	`Function.Surjective.isLocalHom` `ZMod.ringHom_surjective`
`isLocalHom_id` 📖	mathematical	—	`IsLocalHom` `RingHom` `Semiring.toNonAssocSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `RingHom.instFunLike` `RingHom.id`	—	—
`isLocalHom_of_comp` 📖	mathematical	—	`IsLocalHom` `RingHom` `Semiring.toNonAssocSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `RingHom.instFunLike`	—	`isUnit_map_iff` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `RingHom.isUnit_map`
`isLocalHom_toRingHom` 📖	mathematical	—	`IsLocalHom` `RingHom` `Semiring.toNonAssocSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `RingHom.instFunLike` `RingHomClass.toRingHom`	—	`IsLocalHom.map_nonunit`
`map_nonunit` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsLocalRing.maximalIdeal`	`DFunLike.coe` `RingHom` `RingHom.instFunLike`	—	`isUnit_of_map_unit`

---

← Back to Index