instCommMonoidWithZero

Mathlib.Data.EReal.Inv

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

Lean4

instance : CommMonoidWithZero EReal :=
  {
    inferInstanceAs
      (MulZeroOneClass
        EReal) with
    mul_assoc := fun x y z => by
      rw [← sign_eq_and_abs_eq_iff_eq]
      simp only [mul_assoc, abs_mul, sign_mul, and_self_iff]
    mul_comm := EReal.mul_comm }

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

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

Разделы

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

Аффилиация

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