instHasDistribNeg — Mathlib

English

For the unit sphere in a seminormed ring, negation distributes over multiplication. Specifically, for x,y on the unit sphere, (-x)·y = -(x·y) and x·(-y) = -(x·y).

Русский

Для единичной сферы в полугруппе с нормированной нормой отрицание распределяется над умножением: для x,y на единичной сфере выполняются (-x)·y = -(x·y) и x·(-y) = -(x·y).

LaTeX

$$$$\\forall x,y \\in \\mathrm{sphere}(0,1),\\; (-x)\\cdot y = -(x\\cdot y) \\quad \\text{и}\\quad x\\cdot(-y) = -(x\\cdot y).$$$$

Lean4

instance instHasDistribNeg [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] : HasDistribNeg (sphere (0 : 𝕜) 1) :=
  Subtype.coe_injective.hasDistribNeg ((↑) : sphere (0 : 𝕜) 1 → 𝕜) (fun _ => rfl) fun _ _ => rfl

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