Theorem Subsemiring.coe_prod

Modification history

2023-05-28 11:05
Mathlib/RingTheory/Subsemiring/Basic.lean
refactor: use the typeclass `SProd` to implement overloaded notation `· ×ˢ ·` (#4200) …
Modified Subsemiring.coe_prodView on Github →
2023-01-30 11:31
Mathlib/RingTheory/Subsemiring/Basic.lean
feat: port RingTheory.Subsemiring.Basic (#1862)
Added Subsemiring.coe_prodView on Github →