instCommMonoidWithZero

Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

URI: https://scilib.ai/kg/mathlib#Localization.instCommMonoidWithZero

Lean4

instance : CommMonoidWithZero (Localization S)
    where
  zero_mul := fun x ↦
    Localization.induction_on x fun y => by
      simp only [← Localization.mk_zero y.2, mk_mul, mk_eq_mk_iff, mul_zero, zero_mul, r_of_eq]
  mul_zero := fun x ↦
    Localization.induction_on x fun y => by
      simp only [← Localization.mk_zero y.2, mk_mul, mk_eq_mk_iff, mul_zero, r_of_eq]

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

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

Разделы

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

Аффилиация

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