congr_arg

Mathlib.Algebra.Algebra.Equiv

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

English

If f = g as algebra equivalences, then for every x, f x = g x.

Русский

Если f = g как алгебраические эквивалентности, то для каждого x выполняется f x = g x.

LaTeX

$$$f = g \\Rightarrow \\forall x, f x = g x$$$

Lean4

protected theorem congr_arg {f : A₁ ≃ₐ[R] A₂} {x x' : A₁} : x = x' → f x = f x' :=
  DFunLike.congr_arg f

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

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

Разделы

Аффилиация

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