English
The unit sphere in a seminormed ring with strictly multiplicative norm forms a submonoid under multiplication: closed under multiplication and contains 1.
Русский
Единичная сфера в полусферном кольце с строго умножающей нормой образует подмоноид по умножению: замкнута по умножению и содержит 1.
LaTeX
$$$S = \{x \in 𝕜 : \|x\| = 1\} \text{ is a submonoid of } 𝕜 \text{ under multiplication, with } 1 \in S.$$$
Lean4
/-- Unit sphere in a seminormed ring (with strictly multiplicative norm) as a bundled
`Submonoid`. -/
@[simps]
def unitSphere (𝕜 : Type*) [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] : Submonoid 𝕜
where
carrier := sphere (0 : 𝕜) 1
mul_mem' hx
hy := by
rw [mem_sphere_zero_iff_norm] at *
simp [*]
one_mem' := mem_sphere_zero_iff_norm.2 norm_one
