toNoZeroSMulDivisors — Mathlib

English

If R is a GroupWithZero and M is an AddMonoid with a distributive action of R on M, then there is a NoZeroSMulDivisors R M instance (e.g., for Division semirings like NNReal).

Русский

Если R — GroupWithZero и M — аддитивная моноидa с дистрибутивным действием R на M, то существует инстанс NoZeroSMulDivisors R M.

LaTeX

$$NoZeroSMulDivisors R M$$

Lean4

/-- This instance applies to `DivisionSemiring`s, in particular `NNReal` and `NNRat`. -/
instance (priority := 100) toNoZeroSMulDivisors : NoZeroSMulDivisors R M :=
  ⟨fun {a _} h ↦ or_iff_not_imp_left.2 fun ha ↦ (smul_eq_zero_iff_eq <| Units.mk0 a ha).1 h⟩

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