instMonoidWithZero

Mathlib.RingTheory.OreLocalization.Basic

URI: https://scilib.ai/kg/mathlib#OreLocalization.instMonoidWithZero

Lean4

instance : MonoidWithZero R[S⁻¹]
    where
  zero_mul
    x :=
    by
    induction x using OreLocalization.ind with
    | _ r s
    rw [OreLocalization.zero_def, oreDiv_mul_char 0 r 1 s 0 1 (by simp), zero_mul, one_mul]
  mul_zero
    x :=
    by
    induction x using OreLocalization.ind with
    | _ r s
    rw [OreLocalization.zero_def, mul_div_one, mul_zero, zero_oreDiv', zero_oreDiv']

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

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

Разделы

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

Аффилиация

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