instCommSemiring

Mathlib.Algebra.RingQuot

URI: https://scilib.ai/kg/mathlib#RingQuot.instCommSemiring

Lean4

instance instCommSemiring {R : Type uR} [CommSemiring R] (r : R → R → Prop) : CommSemiring (RingQuot r) :=
  { RingQuot.instSemiring r with
    mul_comm := by
      rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
      simp [mul_quot, mul_comm] }

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

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

Разделы

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

Аффилиация

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