ext

Mathlib.Algebra.Algebra.Hom

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

English

If two AlgHoms φ1, φ2 agree on every input, then φ1 = φ2.

Русский

Если два AlgHom совпадают на всех входах, то они равны.

LaTeX

$$$\\forall x, φ_1 x = φ_2 x \\Rightarrow φ_1 = φ_2$$$

Lean4

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

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

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

Разделы

Аффилиация

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