symm_apply_eq

Mathlib.Algebra.Ring.Equiv

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

English

For any ring isomorphism e, the equality e.symm x = y is equivalent to x = e y.

Русский

Для любого кольцевого изоморфизма e равенство e.symm x = y эквивалентно x = e y.

LaTeX

$$$e^{-1}x = y \\iff x = ey$$$

Lean4

theorem symm_apply_eq (e : R ≃+* S) {x : S} {y : R} : e.symm x = y ↔ x = e y :=
  Equiv.symm_apply_eq _

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

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

Разделы

Аффилиация

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