Loogle!

Result

Found 95 declarations mentioning WeierstrassCurve.map.

WeierstrassCurve.map_id 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) : W.map (RingHom.id R) = W
WeierstrassCurve.map 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (f : R →+* A) : WeierstrassCurve A
WeierstrassCurve.instIsEllipticMap 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).IsElliptic
WeierstrassCurve.map_a₁ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).a₁ = f W.a₁
WeierstrassCurve.map_a₂ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).a₂ = f W.a₂
WeierstrassCurve.map_a₃ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).a₃ = f W.a₃
WeierstrassCurve.map_a₄ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).a₄ = f W.a₄
WeierstrassCurve.map_a₆ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).a₆ = f W.a₆
WeierstrassCurve.map_injective 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] {A : Type v} [CommRing A] {f : R →+* A} (hf : Function.Injective ⇑f) : Function.Injective fun W => W.map f
WeierstrassCurve.map_b₂ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).b₂ = f W.b₂
WeierstrassCurve.map_b₄ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).b₄ = f W.b₄
WeierstrassCurve.map_b₆ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).b₆ = f W.b₆
WeierstrassCurve.map_b₈ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).b₈ = f W.b₈
WeierstrassCurve.map_c₄ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).c₄ = f W.c₄
WeierstrassCurve.map_c₆ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).c₆ = f W.c₆
WeierstrassCurve.map_Δ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).Δ = f W.Δ
WeierstrassCurve.map_j 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).j = f W.j
WeierstrassCurve.map_map 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (f : R →+* A) {B : Type w} [CommRing B] (g : A →+* B) : (W.map f).map g = W.map (g.comp f)
WeierstrassCurve.coe_map_Δ' 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {A : Type v} [CommRing A] (f : R →+* A) : ↑(W.map f).Δ' = f ↑W.Δ'
WeierstrassCurve.coe_inv_map_Δ' 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {A : Type v} [CommRing A] (f : R →+* A) : ↑(W.map f).Δ'⁻¹ = f ↑W.Δ'⁻¹
WeierstrassCurve.map_baseChange 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) {S : Type s} [CommRing S] [Algebra R S] {A : Type v} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type w} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (g : A →ₐ[S] B) : (W.baseChange A).map ↑g = W.baseChange B
WeierstrassCurve.map_Δ' 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).Δ' = (Units.map ↑f) W.Δ'
WeierstrassCurve.inv_map_Δ' 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
{R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {A : Type v} [CommRing A] (f : R →+* A) : (W.map f).Δ'⁻¹ = (Units.map ↑f) W.Δ'⁻¹
WeierstrassCurve.map_variableChange 📋 Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
{R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (φ : R →+* A) (C : WeierstrassCurve.VariableChange R) : WeierstrassCurve.VariableChange.map φ C • W.map φ = (C • W).map φ
WeierstrassCurve.map.eq_1 📋 Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
{R : Type u} [CommRing R] (W : WeierstrassCurve R) {A : Type v} [CommRing A] (f : R →+* A) : W.map f = { a₁ := f W.a₁, a₂ := f W.a₂, a₃ := f W.a₃, a₄ := f W.a₄, a₆ := f W.a₆ }
WeierstrassCurve.Affine.map_polynomial 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W : WeierstrassCurve.Affine R} (f : R →+* S) : (WeierstrassCurve.map W f).toAffine.polynomial = Polynomial.map (Polynomial.mapRingHom f) W.polynomial
WeierstrassCurve.Affine.map_polynomialX 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W : WeierstrassCurve.Affine R} (f : R →+* S) : (WeierstrassCurve.map W f).toAffine.polynomialX = Polynomial.map (Polynomial.mapRingHom f) W.polynomialX
WeierstrassCurve.Affine.map_polynomialY 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W : WeierstrassCurve.Affine R} (f : R →+* S) : (WeierstrassCurve.map W f).toAffine.polynomialY = Polynomial.map (Polynomial.mapRingHom f) W.polynomialY
WeierstrassCurve.Affine.Equation.map 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W : WeierstrassCurve.Affine R} (f : R →+* S) {x y : R} (h : W.Equation x y) : (WeierstrassCurve.map W f).toAffine.Equation (f x) (f y)
WeierstrassCurve.Affine.map_equation 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W : WeierstrassCurve.Affine R} {f : R →+* S} (x y : R) (hf : Function.Injective ⇑f) : (WeierstrassCurve.map W f).toAffine.Equation (f x) (f y) ↔ W.Equation x y
WeierstrassCurve.Affine.map_nonsingular 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W : WeierstrassCurve.Affine R} {f : R →+* S} (x y : R) (hf : Function.Injective ⇑f) : (WeierstrassCurve.map W f).toAffine.Nonsingular (f x) (f y) ↔ W.Nonsingular x y
WeierstrassCurve.Affine.map_negPolynomial 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Affine R} (f : R →+* S) : (WeierstrassCurve.map W' f).toAffine.negPolynomial = Polynomial.map (Polynomial.mapRingHom f) W'.negPolynomial
WeierstrassCurve.Affine.map_negY 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Affine R} (f : R →+* S) (x y : R) : (WeierstrassCurve.map W' f).toAffine.negY (f x) (f y) = f (W'.negY x y)
WeierstrassCurve.Affine.map_addPolynomial 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Affine R} (f : R →+* S) (x y ℓ : R) : (WeierstrassCurve.map W' f).toAffine.addPolynomial (f x) (f y) (f ℓ) = Polynomial.map f (W'.addPolynomial x y ℓ)
WeierstrassCurve.Affine.map_addX 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Affine R} (f : R →+* S) (x₁ x₂ ℓ : R) : (WeierstrassCurve.map W' f).toAffine.addX (f x₁) (f x₂) (f ℓ) = f (W'.addX x₁ x₂ ℓ)
WeierstrassCurve.Affine.map_negAddY 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Affine R} (f : R →+* S) (x₁ y₁ x₂ ℓ : R) : (WeierstrassCurve.map W' f).toAffine.negAddY (f x₁) (f x₂) (f y₁) (f ℓ) = f (W'.negAddY x₁ x₂ y₁ ℓ)
WeierstrassCurve.Affine.map_addY 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Affine R} (f : R →+* S) (x₁ y₁ x₂ ℓ : R) : (WeierstrassCurve.map W' f).toAffine.addY (f x₁) (f x₂) (f y₁) (f ℓ) = f ((WeierstrassCurve.toAffine W').addY x₁ x₂ y₁ ℓ)
WeierstrassCurve.Affine.map_slope 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
{F : Type u} {K : Type v} [Field F] [Field K] {W : WeierstrassCurve.Affine F} (f : F →+* K) (x₁ x₂ y₁ y₂ : F) : (WeierstrassCurve.map W f).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂)
WeierstrassCurve.Affine.CoordinateRing.map 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
{R : Type r} {S : Type s} [CommRing R] [CommRing S] (W' : WeierstrassCurve.Affine R) (f : R →+* S) : WeierstrassCurve.Affine.CoordinateRing →+* WeierstrassCurve.Affine.CoordinateRing
WeierstrassCurve.Affine.CoordinateRing.map_injective 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Affine R} {f : R →+* S} (hf : Function.Injective ⇑f) : Function.Injective ⇑(WeierstrassCurve.Affine.CoordinateRing.map W' f)
WeierstrassCurve.Affine.CoordinateRing.map.eq_1 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
{R : Type r} {S : Type s} [CommRing R] [CommRing S] (W' : WeierstrassCurve.Affine R) (f : R →+* S) : WeierstrassCurve.Affine.CoordinateRing.map W' f = AdjoinRoot.lift ((AdjoinRoot.of (WeierstrassCurve.map W' f).toAffine.polynomial).comp (Polynomial.mapRingHom f)) (AdjoinRoot.root (WeierstrassCurve.map W' f).toAffine.polynomial) ⋯
WeierstrassCurve.Affine.CoordinateRing.map_mk 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Affine R} (f : R →+* S) (x : Polynomial (Polynomial R)) : (WeierstrassCurve.Affine.CoordinateRing.map W' f) ((WeierstrassCurve.Affine.CoordinateRing.mk W') x) = (WeierstrassCurve.Affine.CoordinateRing.mk (WeierstrassCurve.map W' f)) (Polynomial.map (Polynomial.mapRingHom f) x)
WeierstrassCurve.Affine.CoordinateRing.map_smul 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Affine R} (f : R →+* S) (x : Polynomial R) (y : WeierstrassCurve.Affine.CoordinateRing) : (WeierstrassCurve.Affine.CoordinateRing.map W' f) (x • y) = Polynomial.map f x • (WeierstrassCurve.Affine.CoordinateRing.map W' f) y
WeierstrassCurve.map_preΨ₄ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) : (W.map f).preΨ₄ = Polynomial.map f W.preΨ₄
WeierstrassCurve.map_Ψ₂Sq 📋 Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) : (W.map f).Ψ₂Sq = Polynomial.map f W.Ψ₂Sq
WeierstrassCurve.map_Ψ₃ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) : (W.map f).Ψ₃ = Polynomial.map f W.Ψ₃
WeierstrassCurve.map_preΨ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ) : (W.map f).preΨ n = Polynomial.map f (W.preΨ n)
WeierstrassCurve.map_preΨ' 📋 Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℕ) : (W.map f).preΨ' n = Polynomial.map f (W.preΨ' n)
WeierstrassCurve.map_Φ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ) : (W.map f).Φ n = Polynomial.map f (W.Φ n)
WeierstrassCurve.map_ΨSq 📋 Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ) : (W.map f).ΨSq n = Polynomial.map f (W.ΨSq n)
WeierstrassCurve.map_ψ₂ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) : (W.map f).ψ₂ = Polynomial.map (Polynomial.mapRingHom f) W.ψ₂
WeierstrassCurve.map_Ψ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ) : (W.map f).Ψ n = Polynomial.map (Polynomial.mapRingHom f) (W.Ψ n)
WeierstrassCurve.map_φ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ) : (W.map f).φ n = Polynomial.map (Polynomial.mapRingHom f) (W.φ n)
WeierstrassCurve.map_ψ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ) : (W.map f).ψ n = Polynomial.map (Polynomial.mapRingHom f) (W.ψ n)
WeierstrassCurve.Jacobian.Equation.map 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S) {P : Fin 3 → R} (h : W'.Equation P) : (WeierstrassCurve.map W' f).toJacobian.Equation (⇑f ∘ P)
WeierstrassCurve.Jacobian.map_equation 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} {f : R →+* S} (P : Fin 3 → R) (hf : Function.Injective ⇑f) : (WeierstrassCurve.map W' f).toJacobian.Equation (⇑f ∘ P) ↔ W'.Equation P
WeierstrassCurve.Jacobian.map_nonsingular 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} {f : R →+* S} (P : Fin 3 → R) (hf : Function.Injective ⇑f) : (WeierstrassCurve.map W' f).toJacobian.Nonsingular (⇑f ∘ P) ↔ W'.Nonsingular P
WeierstrassCurve.Jacobian.map_polynomial 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S) : (WeierstrassCurve.map W' f).toJacobian.polynomial = (MvPolynomial.map f) W'.polynomial
WeierstrassCurve.Jacobian.map_polynomialX 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S) : (WeierstrassCurve.map W' f).toJacobian.polynomialX = (MvPolynomial.map f) W'.polynomialX
WeierstrassCurve.Jacobian.map_polynomialY 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S) : (WeierstrassCurve.map W' f).toJacobian.polynomialY = (MvPolynomial.map f) W'.polynomialY
WeierstrassCurve.Jacobian.map_polynomialZ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S) : (WeierstrassCurve.map W' f).toJacobian.polynomialZ = (MvPolynomial.map f) W'.polynomialZ
WeierstrassCurve.Jacobian.map_dblU 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S) (P : Fin 3 → R) : (WeierstrassCurve.map W' f).toJacobian.dblU (⇑f ∘ P) = f (W'.dblU P)
WeierstrassCurve.Jacobian.map_dblX 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S) (P : Fin 3 → R) : (WeierstrassCurve.map W' f).toJacobian.dblX (⇑f ∘ P) = f (W'.dblX P)
WeierstrassCurve.Jacobian.map_dblY 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S) (P : Fin 3 → R) : (WeierstrassCurve.map W' f).toJacobian.dblY (⇑f ∘ P) = f (W'.dblY P)
WeierstrassCurve.Jacobian.map_dblZ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S) (P : Fin 3 → R) : (WeierstrassCurve.map W' f).toJacobian.dblZ (⇑f ∘ P) = f (W'.dblZ P)
WeierstrassCurve.Jacobian.map_negDblY 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S) (P : Fin 3 → R) : (WeierstrassCurve.map W' f).toJacobian.negDblY (⇑f ∘ P) = f (W'.negDblY P)
WeierstrassCurve.Jacobian.map_negY 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S) (P : Fin 3 → R) : (WeierstrassCurve.map W' f).toJacobian.negY (⇑f ∘ P) = f (W'.negY P)
WeierstrassCurve.Jacobian.map_dblXYZ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S) (P : Fin 3 → R) : (WeierstrassCurve.map W' f).toJacobian.dblXYZ (⇑f ∘ P) = ⇑f ∘ W'.dblXYZ P
WeierstrassCurve.Jacobian.map_addX 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S) (P Q : Fin 3 → R) : (WeierstrassCurve.map W' f).toJacobian.addX (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addX P Q)
WeierstrassCurve.Jacobian.map_addY 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S) (P Q : Fin 3 → R) : (WeierstrassCurve.map W' f).toJacobian.addY (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addY P Q)
WeierstrassCurve.Jacobian.map_negAddY 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S) (P Q : Fin 3 → R) : (WeierstrassCurve.map W' f).toJacobian.negAddY (⇑f ∘ P) (⇑f ∘ Q) = f (W'.negAddY P Q)
WeierstrassCurve.Jacobian.map_addXYZ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S) (P Q : Fin 3 → R) : (WeierstrassCurve.map W' f).toJacobian.addXYZ (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W'.addXYZ P Q
WeierstrassCurve.Jacobian.map_neg 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S) (P : Fin 3 → R) : (WeierstrassCurve.map W' f).toJacobian.neg (⇑f ∘ P) = ⇑f ∘ W'.neg P
WeierstrassCurve.Jacobian.map_add 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
{F : Type u} {K : Type v} [Field F] [Field K] {W : WeierstrassCurve.Jacobian F} (f : F →+* K) {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) : (WeierstrassCurve.map W f).toJacobian.add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q
WeierstrassCurve.Projective.Equation.map 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S) {P : Fin 3 → R} (h : W'.Equation P) : (WeierstrassCurve.map W' f).toProjective.Equation (⇑f ∘ P)
WeierstrassCurve.Projective.map_equation 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} {f : R →+* S} (P : Fin 3 → R) (hf : Function.Injective ⇑f) : (WeierstrassCurve.map W' f).toProjective.Equation (⇑f ∘ P) ↔ W'.Equation P
WeierstrassCurve.Projective.map_nonsingular 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} {f : R →+* S} (P : Fin 3 → R) (hf : Function.Injective ⇑f) : (WeierstrassCurve.map W' f).toProjective.Nonsingular (⇑f ∘ P) ↔ W'.Nonsingular P
WeierstrassCurve.Projective.map_polynomial 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S) : (WeierstrassCurve.map W' f).toProjective.polynomial = (MvPolynomial.map f) W'.polynomial
WeierstrassCurve.Projective.map_polynomialX 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S) : (WeierstrassCurve.map W' f).toProjective.polynomialX = (MvPolynomial.map f) W'.polynomialX
WeierstrassCurve.Projective.map_polynomialY 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S) : (WeierstrassCurve.map W' f).toProjective.polynomialY = (MvPolynomial.map f) W'.polynomialY
WeierstrassCurve.Projective.map_polynomialZ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S) : (WeierstrassCurve.map W' f).toProjective.polynomialZ = (MvPolynomial.map f) W'.polynomialZ
WeierstrassCurve.Projective.map_dblX 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S) (P : Fin 3 → R) : (WeierstrassCurve.map W' f).toProjective.dblX (⇑f ∘ P) = f (W'.dblX P)
WeierstrassCurve.Projective.map_dblY 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S) (P : Fin 3 → R) : (WeierstrassCurve.map W' f).toProjective.dblY (⇑f ∘ P) = f (W'.dblY P)
WeierstrassCurve.Projective.map_dblZ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S) (P : Fin 3 → R) : (WeierstrassCurve.map W' f).toProjective.dblZ (⇑f ∘ P) = f (W'.dblZ P)
WeierstrassCurve.Projective.map_negDblY 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S) (P : Fin 3 → R) : (WeierstrassCurve.map W' f).toProjective.negDblY (⇑f ∘ P) = f (W'.negDblY P)
WeierstrassCurve.Projective.map_negY 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S) (P : Fin 3 → R) : (WeierstrassCurve.map W' f).toProjective.negY (⇑f ∘ P) = f (W'.negY P)
WeierstrassCurve.Projective.map_dblXYZ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S) (P : Fin 3 → R) : (WeierstrassCurve.map W' f).toProjective.dblXYZ (⇑f ∘ P) = ⇑f ∘ W'.dblXYZ P
WeierstrassCurve.Projective.map_dblU 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
{F : Type u} {K : Type v} [Field F] [Field K] {W : WeierstrassCurve.Projective F} (f : F →+* K) (P : Fin 3 → F) : (WeierstrassCurve.map W f).toProjective.dblU (⇑f ∘ P) = f (W.dblU P)
WeierstrassCurve.Projective.map_addX 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S) (P Q : Fin 3 → R) : (WeierstrassCurve.map W' f).toProjective.addX (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addX P Q)
WeierstrassCurve.Projective.map_addY 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S) (P Q : Fin 3 → R) : (WeierstrassCurve.map W' f).toProjective.addY (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addY P Q)
WeierstrassCurve.Projective.map_addZ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S) (P Q : Fin 3 → R) : (WeierstrassCurve.map W' f).toProjective.addZ (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addZ P Q)
WeierstrassCurve.Projective.map_negAddY 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S) (P Q : Fin 3 → R) : (WeierstrassCurve.map W' f).toProjective.negAddY (⇑f ∘ P) (⇑f ∘ Q) = f (W'.negAddY P Q)
WeierstrassCurve.Projective.map_addXYZ 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S) (P Q : Fin 3 → R) : (WeierstrassCurve.map W' f).toProjective.addXYZ (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W'.addXYZ P Q
WeierstrassCurve.Projective.map_neg 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
{R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S) (P : Fin 3 → R) : (WeierstrassCurve.map W' f).toProjective.neg (⇑f ∘ P) = ⇑f ∘ W'.neg P
WeierstrassCurve.Projective.map_add 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
{F : Type u} {K : Type v} [Field F] [Field K] {W : WeierstrassCurve.Projective F} (f : F →+* K) {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) : (WeierstrassCurve.map W f).toProjective.add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision 40fea08