ext

Mathlib.Algebra.Algebra.Equiv

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

English

Two algebra equivalences are equal if they agree on every input element.

Русский

Две алгебраические эквивалентности равны, если они совпадают на каждом элементе.

LaTeX

$$$\\forall a \\in A_1,\\; f(a) = g(a) \\Rightarrow f = g$$$

Lean4

@[ext]
theorem ext {f g : A₁ ≃ₐ[R] A₂} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h

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

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

Разделы

Аффилиация

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