Subring

Statistics

Metric	Count
Definitions	0
Theorems `mem_map_range`, `mem_map_rangeS`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_map_range` 📖	mathematical	—	`Polynomial` `Ring.toSemiring` `Subring` `ring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `mapRingHom` `coeff`	—	`mem_map_rangeS`
`mem_map_rangeS` 📖	mathematical	—	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `RingHom.rangeS` `mapRingHom` `coeff`	—	`coe_mapRingHom` `coeff_map` `Set.mem_range_self` `as_sum_range_C_mul_X_pow` `Subsemiring.sum_mem` `map_mul` `map_C` `map_pow` `map_X`

---