toMul

Mathlib.Algebra.Group.TypeTags.Basic

URI: https://scilib.ai/kg/mathlib#Additive.toMul

English

There is a canonical equivalence Additive α ≃ α, reversing ofMul.

Русский

Существует каноническое эквивалентное отображение Additive α ≃ α, обратное toMul.

LaTeX

$$$\text{Additive.toMul}: \mathrm{Additive}\alpha \simeq \alpha$$$

Lean4

/-- Reinterpret `x : Additive α` as an element of `α`. -/
def toMul : Additive α ≃ α :=
  ofMul.symm

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

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

Разделы

Аффилиация

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