mk_zero — Mathlib

English

In the Ore localization of a commutative monoid with zero by a submonoid S, for every x in S, the element with numerator 0 and denominator x is equal to 0; i.e., 0/(x) = 0.

Русский

В локализации по Ore моноида с нулём S, для любого x в S элемент с числителем 0 и знаменателем x равен нулю; то есть 0/x = 0.

LaTeX

$$$\forall x \in S:\ 0/x = 0$$$

Lean4

theorem mk_zero (x : S) : mk 0 (x : S) = 0 :=
  OreLocalization.zero_oreDiv' _

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