instInhabitedOfIsOrderedAddMonoid

Mathlib.Algebra.Order.Module.HahnEmbedding

URI: https://scilib.ai/kg/mathlib#HahnEmbedding.Partial.instInhabitedOfIsOrderedAddMonoid

Lean4

noncomputable instance [IsOrderedAddMonoid R] : Inhabited (Partial seed) where
  default := ⟨seed.baseEmbedding, seed.isPartial_baseEmbedding⟩

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

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

Разделы

Аффилиация

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