eqLocus

Mathlib.RingTheory.NonUnitalSubring.Basic

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

Lean4

/-- The `NonUnitalSubring` of elements `x : R` such that `f x = g x`, i.e.,
  the equalizer of f and g as a `NonUnitalSubring` of R -/
def eqLocus (f g : R →ₙ+* S) : NonUnitalSubring R :=
  { (f : R →ₙ* S).eqLocus g, (f : R →+ S).eqLocus g with carrier := {x | f x = g x} }

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

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

Разделы

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

Аффилиация

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