mulOneClass — Mathlib

English

If α has a MulOneClass, then Finset α inherits a MulOneClass under the pointwise product.

Русский

Если α имеет структуру MulOneClass, то Finset α наследует MulOneClass при точечном умножении.

LaTeX

$$$$ \\text{Finset }\\alpha \\text{ has a } MulOneClass \\text{ if } \\alpha \\text{ does.} $$$$

Lean4

/-- `Finset α` is a `MulOneClass` under pointwise operations if `α` is. -/
@[to_additive /-- `Finset α` is an `AddZeroClass` under pointwise operations if `α` is. -/
    ]
protected def mulOneClass : MulOneClass (Finset α) :=
  coe_injective.mulOneClass _ (coe_singleton 1) coe_mul

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