instContinuousStarUnits — Mathlib

English

The group of units Rˣ inherits a ContinuousStar instance from ContinuousStar R via induced structure.

Русский

Группа единиц Rˣ наследует ContinuousStar от R через индуцированную структуру.

LaTeX

$$$\mathrm{ContinuousStar}(\mathrm{Units}(R))$$$

Lean4

instance [Monoid R] [StarMul R] [TopologicalSpace R] [ContinuousStar R] : ContinuousStar Rˣ :=
  ⟨continuous_induced_rng.2 Units.continuous_embedProduct.star⟩

Похожие утверждения