divisionMonoid — Mathlib

English

If α is a division monoid, Finset α forms a division monoid under pointwise operations.

Русский

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

LaTeX

$$Finset divisionMonoid: [DivisionMonoid α] ⇒ DivisionMonoid (Finset α)$$

Lean4

/-- `Finset α` is a division monoid under pointwise operations if `α` is. -/
@[to_additive /-- `Finset α` is a subtraction monoid under pointwise operations if `α` is. -/
    ]
protected def divisionMonoid : DivisionMonoid (Finset α) :=
  coe_injective.divisionMonoid _ coe_one coe_mul coe_inv coe_div coe_pow coe_zpow

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