English
The commutative monoid structure on Interval α is transported along the isomorphism toProd, yielding equivalence to the standard product structure.
Русский
Комм-Моноид на Interval α переносится вдоль изоморфизма toProd, образуя эквивалентность стандартной структуре произведения.
LaTeX
$$$\\text{Eq Interval.commMonoid (Function.Injective.commMonoid ...)}$$$
Lean4
@[to_additive]
instance mulOneClass [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] : MulOneClass (Interval α)
where
mul := (· * ·)
one := 1
one_mul s := (WithBot.map₂_coe_left _ _ _).trans <| by simp_rw [one_mul, ← Function.id_def, WithBot.map_id, id]
mul_one s := (WithBot.map₂_coe_right _ _ _).trans <| by simp_rw [mul_one, ← Function.id_def, WithBot.map_id, id]
