ext

Mathlib.RingTheory.Bialgebra.Hom

URI: https://scilib.ai/kg/mathlib#BialgHom.ext

English

Two homomorphisms are equal if they agree on every input.

Русский

Гомоморфизмы равны, если совпадают на каждом входе.

LaTeX

$$$\\forall x,\\; \\phi_1(x) = \\phi_2(x) \\Rightarrow \\phi_1 = \\phi_2$$$

Lean4

@[ext]
theorem ext {φ₁ φ₂ : A →ₐc[R] B} (H : ∀ x, φ₁ x = φ₂ x) : φ₁ = φ₂ :=
  DFunLike.ext _ _ H

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

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

Разделы

Аффилиация

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