instDistrib — Mathlib

English

The operations on Fin n satisfy distributivity: left and right distributive laws hold.

Русский

Операции на Fin n удовлетворяют распределительности: слева и справа выполняются законы распределения.

LaTeX

$$$\forall a,b,c:\ (a+b)\cdot c = a\cdot c + b\cdot c \wedge a\cdot(b+c) = a\cdot b + a\cdot c$$$

Lean4

/-- Distributive structure on `Fin n`. -/
instance instDistrib (n : ℕ) : Distrib (Fin n) :=
  { Fin.addCommSemigroup n,
    Fin.instCommSemigroup n with
    left_distrib := left_distrib_aux n
    right_distrib := fun a b c => by rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm] }

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