instHasDistribNeg — Mathlib

English

If G has a distributive negation with multiplication, then Germ l G inherits it: - distributes over multiplication in germs.

Русский

Если у G есть распределительное отрицание относительно умножения, то у Germ l G оно также есть: (-q1)·q2 = -(q1·q2) и q1·(-q2) = -(q1·q2).

LaTeX

$$$ (-q_1) \\cdot q_2 = -(q_1 \\cdot q_2), \\quad q_1 \\cdot (-q_2) = -(q_1 \\cdot q_2). $$$

Lean4

instance instHasDistribNeg [Mul G] [HasDistribNeg G] : HasDistribNeg (Germ l G) :=
  { neg_mul := Quotient.ind₂' fun _ _ => congrArg ofFun <| neg_mul ..
    mul_neg := Quotient.ind₂' fun _ _ => congrArg ofFun <| mul_neg .. }

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