instHasDistribNeg — Mathlib

English

The unit group αˣ carries a HasDistribNeg structure derived from the base ring via val_neg and val_mul.

Русский

Группа единиц αˣ получает структуру HasDistribNeg, вытекающую из базового кольца через val_neg и val_mul.

LaTeX

$$$HasDistribNeg(\alpha^{\times})$ with neg defined by $u \mapsto \langle -\text{val}(u), -\text{val}(u)^{-1}, \dots \rangle$ and compatible with multiplication.$$

Lean4

instance : HasDistribNeg αˣ :=
  val_injective.hasDistribNeg _ Units.val_neg val_mul

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