mulOneClass — Mathlib

English

Set α inherits a MulOneClass structure from α when α has one and multiplication.

Русский

Set α наследует структуру MulOneClass от α, если в α есть единица и умножение.

LaTeX

$$$$ \text{Set } α \text{ is a } MulOneClass \text{ when } α \text{ is a } MulOneClass. $$$$

Lean4

/-- `Set α` is a `MulOneClass` under pointwise operations if `α` is. -/
@[to_additive /-- `Set α` is an `AddZeroClass` under pointwise operations if `α` is. -/
    ]
protected def mulOneClass : MulOneClass (Set α) :=
  { Set.one, Set.mul with
    mul_one := image2_right_identity mul_one
    one_mul := image2_left_identity one_mul }

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