ofEq_symm

Mathlib.Algebra.Module.Submodule.Equiv

URI: https://scilib.ai/kg/mathlib#LinearEquiv.ofEq_symm

English

If p = q, then the corresponding linear equivalence sends x in p to x in M unchanged.

Русский

Если p = q, то соответствующее линейное эквивалентное отображение отправляет x в p в x в M без изменений.

LaTeX

$$coe_ofEq_apply (h : p = q) (x : p) : (ofEq p q h x : M) = x$$

Lean4

@[simp]
theorem ofEq_symm (h : p = q) : (ofEq p q h).symm = ofEq q p h.symm :=
  rfl

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

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

Разделы

Аффилиация

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