nonZeroDivisors

Mathlib.Algebra.GroupWithZero.NonZeroDivisors

URI: https://scilib.ai/kg/mathlib#nonZeroDivisors

Lean4

/-- The submonoid of non-zero-divisors of a `MonoidWithZero` `M₀`. -/
def nonZeroDivisors (M₀ : Type*) [MonoidWithZero M₀] : Submonoid M₀ :=
  nonZeroDivisorsLeft M₀ ⊓ nonZeroDivisorsRight M₀

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru