map_equation — Mathlib

English

If f is an injective ring homomorphism, then a point (x, y) lies on W if and only if its image (f x, f y) lies on the image curve W.map f.

Русский

Если f инъективно отображает кольца, то точка (x, y) лежит на W тогда и только тогда, когда её образ (f x, f y) лежит на кривой W.map f.

LaTeX

$$$\text{hf injective} \Rightarrow (W.map f).toAffine.Equation (f x) (f y) \iff W.Equation x y$$$

Lean4

theorem map_equation (hf : Function.Injective f) : (W.map f).toAffine.Equation (f x) (f y) ↔ W.Equation x y := by
  simp only [Equation, map_polynomial, map_mapRingHom_evalEval, map_eq_zero_iff f hf]

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