instNonUnitalCommRing — Mathlib

English

Fin n forms a nonunital commutative ring when n ≠ 0, i.e., it has addition, multiplication, and zero with zero absorbing properties but no required multiplicative identity.

Русский

Fin n образует немодулярное (неассоциированное) кольцо, если n ≠ 0: есть сложение, умножение и ноль, с нулём, как нулём поглощения, но не обязательно единица.

LaTeX

$$$\text{NonUnitalCommRing}(\text{Fin } n)$$$

Lean4

instance instNonUnitalCommRing (n : ℕ) [NeZero n] : NonUnitalCommRing (Fin n)
    where
  __ := Fin.addCommGroup n
  __ := Fin.instCommSemigroup n
  __ := Fin.instDistrib n
  zero_mul := Fin.zero_mul'
  mul_zero := Fin.mul_zero'

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