toNonAssocSemiring

Mathlib.Algebra.Ring.Subsemiring.Defs

URI: https://scilib.ai/kg/mathlib#SubsemiringClass.toNonAssocSemiring

Lean4

/-- A subsemiring of a `NonAssocSemiring` inherits a `NonAssocSemiring` structure -/
instance (priority := 75) toNonAssocSemiring : NonAssocSemiring s :=
  fast_instance%Subtype.coe_injective.nonAssocSemiring Subtype.val rfl rfl (fun _ _ => rfl) (fun _ _ => rfl)
      (fun _ _ => rfl) fun _ => rfl

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

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

Разделы

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

Аффилиация

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