mem_equalizer

Mathlib.Algebra.Star.Subalgebra

URI: https://scilib.ai/kg/mathlib#StarAlgHom.mem_equalizer

English

Same as mem_equalizer, in a variant simp form.

Русский

То же, что mem_equalizer, в форме simp.

LaTeX

$$$ x \\in StarAlgHom.equalizer f g \\iff f x = g x $$$

Lean4

@[simp]
theorem mem_equalizer (x : A) : x ∈ StarAlgHom.equalizer f g ↔ f x = g x :=
  Iff.rfl

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

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

Разделы

Аффилиация

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