ofMul — Mathlib

English

There is a canonical equivalence between α and Additive α, given by identity on underlying type.

Русский

Существует каноническое эквивалентное отображение между α и Additive α, задающееся тождественным отображением на базовом типе.

LaTeX

$$$\text{Additive.ofMul}: \alpha \simeq Additive\alpha$$$

Lean4

/-- Reinterpret `x : α` as an element of `Additive α`. -/
def ofMul : α ≃ Additive α :=
  ⟨fun x => x, fun x => x, fun _ => rfl, fun _ => rfl⟩

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