Subring

Statistics

Metric	Count
Definitions	0
Theorems `of_injective`, `of_subring`, `of_subring'`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`of_injective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`IsLocalRing`	—	`RingHom.domain_nontrivial` `toNontrivial` `mem_nonZeroDivisors_of_injective` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsUnit.mem_nonZeroDivisors` `isUnit_or_isUnit_of_add_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass`
`of_subring` 📖	mathematical	`IsUnit` `Subsemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Subsemiring.toSemiring`	`IsLocalRing`	—	`of_injective` `Subsemiring.subtype_injective`
`of_subring'` 📖	mathematical	`Subsemiring` `Semiring.toNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Subsemiring.instPartialOrder` `IsUnit` `SetLike.instMembership` `Subsemiring.instSetLike` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Subsemiring.toSemiring`	`IsLocalRing`	—	`of_injective` `Subsemiring.inclusion_injective`

---