toEquiv

Mathlib.Algebra.Algebra.Equiv

URI: https://scilib.ai/kg/mathlib#AlgEquiv.Simps.toEquiv

English

The underlying equivalence of an algebra equivalence is the same as the associated Equiv.

Русский

Упрощённая эквивалентность алгебровой эквивалентности совпадает с ассоциированной эквив.

LaTeX

$$$\text{toEquiv}(e) = e$$$

Lean4

/-- See Note [custom simps projection] -/
def toEquiv (e : A₁ ≃ₐ[R] A₂) : A₁ ≃ A₂ :=
  e

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

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

Разделы

Аффилиация

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