instHasDistribNeg — Mathlib

English

Negation distributes over multiplication in Pell.Solution₁ d: for all a,b, -(a b) = (-a) b = a (-b).

Русский

Отрицание распределяется по умножению в Pell.Solution₁ d: для любых a,b верно -(a b) = (-a) b = a (-b).

LaTeX

$$$$ \forall a,b \in Pell.Solution_1(d),\ (-a)\cdot b = -(a\cdot b) \quad\text{and}\quad a\cdot(-b) = -(a\cdot b). $$$$

Lean4

instance instHasDistribNeg : HasDistribNeg (Solution₁ d) :=
  inferInstanceAs (HasDistribNeg (unitary (ℤ√d)))

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