mk_coe — Mathlib

English

Let σ be a ring hom and f a σ-linear map with a chosen witness h for its construction via the constructor mk. Then the map obtained by mk with data f and h is exactly f; i.e., mk f h equals f as a σ-linear map.

Русский

Пусть σ — гомомор ring и f — σ-линейное отображение с заданным представлением через конструктор mk. Тогда отображение, полученное конструктором mk из данных f и h, равно f; то есть mk f h = f как σ-линейное отображение.

LaTeX

$$$ (\mathrm{mk} \ f \ h) = f $$$

Lean4

@[simp]
theorem mk_coe (f : M →ₛₗ[σ] M₃) (h) : (mk f h : M →ₛₗ[σ] M₃) = f :=
  rfl

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