English
For a division monoid α, a filter f is a unit with respect to the pointwise multiplication iff f is the principal filter at some unit a of α.
Русский
Для делимого моноида α фильтр f является единицей по точечной умножению тогда и только тогда, когда f — первичный фильтр в отношении некоторого модуля a, для которого a является единицей в α.
LaTeX
$$IsUnit f ↔ ∃ a, f = pure a ∧ IsUnit a$$
Lean4
@[to_additive]
theorem isUnit_iff : IsUnit f ↔ ∃ a, f = pure a ∧ IsUnit a :=
by
constructor
· rintro ⟨u, rfl⟩
obtain ⟨a, b, ha, hb, h⟩ := Filter.mul_eq_one_iff.1 u.mul_inv
refine ⟨a, ha, ⟨a, b, h, pure_injective ?_⟩, rfl⟩
rw [← pure_mul_pure, ← ha, ← hb]
exact u.inv_mul
· rintro ⟨a, rfl, ha⟩
exact ha.filter
