congr_arg

Mathlib.Algebra.Ring.Equiv

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

English

If f is a ring equivalence, then congr_arg preserves equality under f.

Русский

Для кольцевого эквивалента f сохранение равенства под действием f сохраняется: если x = x', то f x = f x'.

LaTeX

$$congr_arg {f : R ≃+* S} {x x' : R} : x = x' → f x = f x'$$

Lean4

protected theorem congr_arg {f : R ≃+* S} {x x' : R} : x = x' → f x = f x' :=
  DFunLike.congr_arg f

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

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

Разделы

Аффилиация

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