English
In a star-monoid, the set of elements U such that star U · U = 1 and U · star U = 1 forms a submonoid, called the unitary elements.
Русский
В звездо-монсиде множество элементов U, удовлетворяющих star U · U = 1 и U · star U = 1, образуют подмоноид, называемый унитарными элементами.
LaTeX
$$$\mathrm{unitary}(R) = \{ U \in R \mid \star U \cdot U = 1 \ \\land U \cdot \star U = 1\}$$$
Lean4
/-- In a *-monoid, `unitary R` is the submonoid consisting of all the elements `U` of
`R` such that `star U * U = 1` and `U * star U = 1`.
-/
def unitary (R : Type*) [Monoid R] [StarMul R] : Submonoid R
where
carrier := {U | star U * U = 1 ∧ U * star U = 1}
one_mem' := by simp only [mul_one, and_self_iff, Set.mem_setOf_eq, star_one]
mul_mem' :=
@fun U B ⟨hA₁, hA₂⟩ ⟨hB₁, hB₂⟩ => by
refine ⟨?_, ?_⟩
·
calc
star (U * B) * (U * B) = star B * star U * U * B := by simp only [mul_assoc, star_mul]
_ = star B * (star U * U) * B := by rw [← mul_assoc]
_ = 1 := by rw [hA₁, mul_one, hB₁]
·
calc
U * B * star (U * B) = U * B * (star B * star U) := by rw [star_mul]
_ = U * (B * star B) * star U := by simp_rw [← mul_assoc]
_ = 1 := by rw [hB₂, mul_one, hA₂]
