zeroEquiv_naturality — Mathlib

English

There is a naturality relation of zeroEquiv with map: (zeroEquiv R N) ∘ (map 0 f) = zeroEquiv R M

Русский

Существуют естественные соотношения нулевой эквивалентности и отображения: (zeroEquiv R N) ∘ (map 0 f) = zeroEquiv R M.

LaTeX

$$$ (zeroEquiv \\ R N) \\circ (map 0 f) = zeroEquiv \\ R M$$$

Lean4

theorem zeroEquiv_naturality (f : M →ₗ[R] N) : (zeroEquiv R N).comp (map 0 f) = zeroEquiv R M := by aesop

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