eqSlocus

Mathlib.RingTheory.NonUnitalSubsemiring.Defs

URI: https://scilib.ai/kg/mathlib#NonUnitalRingHom.eqSlocus

Lean4

/-- The non-unital subsemiring of elements `x : R` such that `f x = g x` -/
def eqSlocus (f g : F) : NonUnitalSubsemiring R :=
  { (f : R →ₙ* S).eqLocus (g : R →ₙ* S), (f : R →+ S).eqLocusM g with carrier := {x | f x = g x} }

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

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

Разделы

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

Аффилиация

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