uniqueProd_symm_apply — Mathlib

English

Let N be a type with a unique element and M a type with an R-module structure. The inverse of the canonical isomorphism between M × N and M sends an element x ∈ M to the pair (n0, x), where n0 is the unique element of N.

Русский

Пусть N — типа с единственным элементом, и M — множество с модульной структурой над R. Обратное отображение к каноническому изоморфизму между M × N и M отправляет элемент x ∈ M в пару (n0, x), где n0 — единственный элемент N.

LaTeX

$$$ (\\text{uniqueProd } R\, M\, N)^{-1}(x) = (n_0, x) $, где $n_0$ — единственный элемент $N$.$$

Lean4

@[simp]
theorem uniqueProd_symm_apply (x : M) : (uniqueProd R M N).symm x = (default, x) :=
  rfl

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