map_zero — Mathlib

English

For any commutative ring R, submonoid S of R, P, and P' with algebra structures over R, and any AlgHom g : P →ₐ[R] P', the image of the zero fractional ideal is the zero fractional ideal, i.e. map g of 0 is 0.

Русский

Для любой коммутативной кольца R, подмонойки S ⊆ R, модулей P и P' с структурой алгебр над R и любой гомоморфизм AlgHom g: P →ₐ[R] P' выполняется: образ нулевого дробного идеала равен нулю, то есть map g(0) = 0.

LaTeX

$$$ (0 : \\mathrm{FractionalIdeal} S P).\\mathrm{map} \\\\ g = 0 $$$

Lean4

@[simp]
protected theorem map_zero : (0 : FractionalIdeal S P).map g = 0 :=
  map_coeIdeal g 0

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