coe_symm

Mathlib.GroupTheory.GroupExtension.Defs

URI: https://scilib.ai/kg/mathlib#GroupExtension.Equiv.coe_symm

English

The coercion of the symmetric equivalence equals the symmetric equivalence.

Русский

Коэрциона симметричной эквивалентности равна симметричной эквивалентности.

LaTeX

$$$ (equiv : E \\simeq^* E').symm = equiv.symm$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_symm : (equiv : E ≃* E').symm = equiv.symm :=
  rfl

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

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

Разделы

Аффилиация

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