English
If α is a DivisionCommMonoid, then Filter α is a DivisionCommMonoid under pointwise operations.
Русский
Если α — коммутативный делимый моноид, то Filter α под покомпонентными операциями образует коммутативный делимый моноид.
LaTeX
$$[DivisionCommMonoid \\ α] \\Rightarrow \\mathrm{DivisionCommMonoid}(\\mathrm{Filter}(\\alpha))$$
Lean4
/-- `Filter α` is a commutative division monoid under pointwise operations if `α` is. -/
@[to_additive subtractionCommMonoid /--
`Filter α` is a commutative subtraction monoid under pointwise operations if `α` is. -/
]
protected def divisionCommMonoid [DivisionCommMonoid α] : DivisionCommMonoid (Filter α) :=
{ Filter.divisionMonoid, Filter.commSemigroup with }
