equation_some — Mathlib

English

For any a,b ∈ R, the triple [a,b,1] lies on the Weierstrass curve W' if and only if the affine equation a, b satisfy W'.toAffine.Equation a b.

Русский

Для любых a,b ∈ R тройка [a,b,1] лежит на кривой Вейерштрасса W', тогда как аффинное уравнение a,b удовлетворяет W'.toAffine.Equation a b.

LaTeX

$$$W'.Equation([a,b,1]) \\iff W'.toAffine.Equation(a,b)$$$

Lean4

theorem equation_some (a b : R) : W'.Equation ![a, b, 1] ↔ W'.toAffine.Equation a b := by
  simp only [equation_iff, Affine.equation_iff', fin3_def_ext, one_pow, mul_one]

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