English
Let n be a natural number. For all x, y in Fin(n), negation distributes over multiplication: -(x y) = (-x) y = x (-y). This holds vacuously when Fin(n) is empty (i.e., n = 0).
Русский
Пусть n — натуральное число. Для любых x, y ∈ Fin(n) выполняется: −(xy) = (−x)y = x(−y). Это равенство тривиально истинно, если Fin(n) пусто (n = 0).
LaTeX
$$$\forall n \in \mathbb{N}, \forall x,y \in \mathrm{Fin}(n):\; -(x\cdot y) = (-x)\cdot y = x\cdot(-y).$$$
Lean4
/-- Note this is more general than `Fin.instCommRing` as it applies (vacuously) to `Fin 0` too. -/
instance instHasDistribNeg (n : ℕ) : HasDistribNeg (Fin n)
where
toInvolutiveNeg := Fin.instInvolutiveNeg n
mul_neg := Nat.casesOn n finZeroElim fun _i => mul_neg
neg_mul := Nat.casesOn n finZeroElim fun _i => neg_mul
