divisionCommMonoid — Mathlib

English

If α is a DivisionCommMonoid, then Set α is a DivisionCommMonoid under pointwise operations.

Русский

Если α является коммутативным дивизионным моноидом, то Set α образует коммутативный дивизионный моноид с точечно заданными операциями.

LaTeX

$$Set.divisionCommMonoid [DivisionCommMonoid α] : DivisionCommMonoid (Set α)$$

Lean4

/-- `Set α` is a commutative division monoid under pointwise operations if `α` is. -/
@[to_additive subtractionCommMonoid /--
    `Set α` is a commutative subtraction monoid under pointwise operations if `α` is. -/
    ]
protected def divisionCommMonoid [DivisionCommMonoid α] : DivisionCommMonoid (Set α) :=
  { Set.divisionMonoid, Set.commSemigroup with }

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