coe_toEquiv

Mathlib.Algebra.Algebra.Equiv

URI: https://scilib.ai/kg/mathlib#AlgEquiv.coe_toEquiv

English

Equality of the underlying Equiv is consistent with equivalence coercions.

Русский

Равенство базовой эквивалентности согласовано с приведениями эквивалентности.

LaTeX

$$$e.toEquiv = EquivLike.toEquiv e$$$

Lean4

@[simp]
theorem coe_toEquiv : ((e : A₁ ≃ A₂) : A₁ → A₂) = e :=
  rfl

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

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

Разделы

Аффилиация

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