instDiv — Mathlib

English

The closed unit ball is a monoid with zero under multiplication; this is the inherited algebraic structure from the ambient ring.

Русский

Замкнутый шар единицы образует моноид с нулём по умножению; это структура кольца, ограниченная шаром.

LaTeX

$$$\text{MonoidWithZero} (\overline{B}(0,1))$ under multiplication$$

Lean4

instance instDiv [NormedDivisionRing 𝕜] : Div (sphere (0 : 𝕜) 1) where
  div x
    y :=
    .mk (x / y) <|
      mem_sphere_zero_iff_norm.2 <| by
        rw [norm_div, mem_sphere_zero_iff_norm.1 x.2, mem_sphere_zero_iff_norm.1 y.coe_prop, div_one]

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