English
If α is a division monoid, then Filter α carries a division monoid structure under the pointwise operations (multiplication, inverse, and division) derived from α.
Русский
Если α — делимый моноид, то Filter α наследует структуру делимого моноида под покомпонентными операциями (умножение, обратное и деление), порожденными α.
LaTeX
$$$[DivisionMonoid \\ α] \\Rightarrow \\mathrm{DivisionMonoid}(\\mathrm{Filter}(\\alpha))$$$
Lean4
/-- `Filter α` is a division monoid under pointwise operations if `α` is. -/
@[to_additive /-- `Filter α` is a subtraction monoid under pointwise operations if `α` is. -/
]
protected def divisionMonoid : DivisionMonoid (Filter α) :=
{ Filter.monoid, Filter.instInvolutiveInv, Filter.instDiv,
Filter.instZPow (α := α) with
mul_inv_rev := fun _ _ => map_map₂_antidistrib mul_inv_rev
inv_eq_of_mul := fun s t h =>
by
obtain ⟨a, b, rfl, rfl, hab⟩ := Filter.mul_eq_one_iff.1 h
rw [inv_pure, inv_eq_of_mul_eq_one_right hab]
div_eq_mul_inv := fun _ _ => map_map₂_distrib_right div_eq_mul_inv }
