ofDual_one — Mathlib

English

Let α be a type with a multiplicative identity 1. The dual construction preserves this identity: the image of 1 under the dual map is equal to 1.

Русский

Пусть у типа α имеется единица умножения 1. Двойственная конструкция сохраняет эту единицу: образ 1 под двойственным отображением равен 1.

LaTeX

$$$ toDual(1) = 1 $$$

Lean4

@[to_additive (attr := simp)]
theorem ofDual_one [One α] : (ofDual 1 : α) = 1 :=
  rfl

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