instMulOneClass — Mathlib

English

The product M × N inherits MulOneClass: left and right identity laws hold componentwise.

Русский

Произведение M × N наследует структуру MulOneClass: левые и правые единицы работают по компонентам.

LaTeX

$$[MulOneClass M] [MulOneClass N] ⇒ M × N is MulOneClass$$

Lean4

@[to_additive]
instance instMulOneClass [MulOneClass M] [MulOneClass N] : MulOneClass (M × N)
    where
  one_mul _ := by ext <;> exact one_mul _
  mul_one _ := by ext <;> exact mul_one _

Похожие утверждения