map_zero — Mathlib

English

The map induced by the identity algebra homomorphism acts trivially on Weierstrass affine points.

Русский

Отображение, индуцированное тождественным алгебраическим гомоморфизмом, действует тривиально на точках аффинной кривой Вейерштрасса.

LaTeX

$$$\mathrm{map}(\mathrm{id})=\mathrm{id}$ on $W'⟮F⟯$$$

Lean4

theorem map_zero : map f (0 : W'⟮F⟯) = 0 :=
  rfl

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