unitsEquivAut_symm_apply

Mathlib.Topology.Algebra.Module.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousLinearEquiv.unitsEquivAut_symm_apply

English

Symmetry: the inverse of a CL equivalence applied to e equals applying the inverse data to e.

Русский

Симметрия: обратное к непрерывно-линейному эквиваленту применяется через данные обратного.

LaTeX

$$$\\text{unitsEquivAut\\_symm\\_apply}(e) = e^{-1}$$$

Lean4

@[simp]
theorem unitsEquivAut_symm_apply (e : R ≃L[R] R) : ↑((unitsEquivAut R).symm e) = e 1 :=
  rfl

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

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

Разделы

Аффилиация

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