Y_eq_of_X_eq — Mathlib

English

If f is injective, then W.baseChange W B at (f x, f y) satisfies the pulled-back equation if and only if W.baseChange W A at (x, y) does.

Русский

Если f инъективно, то уравнение, удовлетворяемое (f x, f y) на W.baseChange B, равно уравнению, удовлетворяемому (x, y) на W.baseChange A.

LaTeX

$$$(W.baseChange W B).toAffine.Equation (f x) (f y) \iff (W.baseChange W A).toAffine.Equation x y$$$

Lean4

theorem Y_eq_of_X_eq {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hx : x₁ = x₂) :
    y₁ = y₂ ∨ y₁ = W.negY x₂ y₂ := by
  rw [equation_iff] at h₁ h₂
  rw [← sub_eq_zero, ← sub_eq_zero (a := y₁), ← mul_eq_zero, negY]
  linear_combination (norm := (rw [hx]; ring1)) h₁ - h₂

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