English
If α is a MulOneClass, then Filter α is a MulOneClass; the unit is 1 and multiplication is pointwise; left and right identities hold.
Русский
Если α имеет структуру MulOneClass, то Filter α также обладает MulOneClass; единица равна 1, умножение — точечное, выполняются левый и правый единицы.
LaTeX
$$$\forall f \in \mathrm{Filter}(\alpha),\ 1 * f = f \;\wedge\; f * 1 = f.$$$
Lean4
/-- `Filter α` is a `MulOneClass` under pointwise operations if `α` is. -/
@[to_additive /-- `Filter α` is an `AddZeroClass` under pointwise operations if `α` is. -/
]
protected def mulOneClass : MulOneClass (Filter α) where
one := 1
mul := (· * ·)
one_mul := map₂_left_identity one_mul
mul_one := map₂_right_identity mul_one
