ofAdd — Mathlib

English

Let α be a type. There exists a natural equivalence between α and Multiplicative α, given by the identity on the underlying elements.

Русский

Пусть α — множество. Существует естественное эквивалентство между α и Multiplicative α, задаваемое идентичностью на элементарной основе.

LaTeX

$$$\alpha \cong \mathrm{Multiplicative}\,\alpha$$$

Lean4

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

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