English
In a division monoid, IsUnit s holds iff s is a singleton {a} for some a that is a unit.
Русский
В делении моноида IsUnit s эквивалентно тому, что s — одиночное множество {a}, где a является единицей.
LaTeX
$$IsUnit s ↔ ∃ a, s = { a } ∧ IsUnit a$$
Lean4
/-- `Set α` is a division monoid under pointwise operations if `α` is. -/
@[to_additive /-- `Set α` is a subtraction monoid under pointwise operations if `α` is. -/
]
protected def divisionMonoid : DivisionMonoid (Set α) :=
{ Set.monoid, Set.involutiveInv, Set.div,
@Set.ZPow α _ _
_ with
mul_inv_rev := fun s t => by
simp_rw [← image_inv_eq_inv]
exact image_image2_antidistrib mul_inv_rev
inv_eq_of_mul := fun s t h => by
obtain ⟨a, b, rfl, rfl, hab⟩ := Set.mul_eq_one_iff.1 h
rw [inv_singleton, inv_eq_of_mul_eq_one_right hab]
div_eq_mul_inv := fun s t => by
rw [← image_id (s / t), ← image_inv_eq_inv]
exact image_image2_distrib_right div_eq_mul_inv }
