alreadydone

import analysis.bounded_variation
import topology.path_connected
/- Authors: Rémi Bottinelli, Junyan Xu -/

open_locale ennreal big_operators
noncomputable theory

section arclength

variables {α E : Type*} [linear_order α] [pseudo_emetric_space E] (f : α → E) {a b c : α}

alreadydone

import topology.uniform_space.basic
import topology.homeomorph

open_locale topological_space uniformity filter
open filter uniform_space set

variables {α β : Type*} [uniform_space α] [uniform_space β]

lemma is_compact.nhds_set_diagonal₁ {α} [uniform_space α] {s : set α} (hs : is_compact s) :
  𝓝ˢ ((λ x, (x, x)) '' s) = 𝓤 α ⊓ 𝓝ˢ (prod.fst ⁻¹' s) := 

alreadydone

import data.polynomial.ring_division

structure EllipticCurve (K : Type*) := (a₁ a₂ a₃ a₄ a₆ : K)

variables {K : Type*} (E : EllipticCurve K)

namespace polynomial
open_locale polynomial

noncomputable def weierstrass_polynomial [ring K] : K[X][X] :=

alreadydone

import data.finsupp.lex
import logic.hydra

variables {α N : Type*} (r : α → α → Prop) (s : N → N → Prop)

namespace finsupp
open relation prod

variable [has_zero N]

alreadydone

variables {α : Sort*} {r : α → α → Prop} {C : α → Sort*} (x : α) (acx : acc r x)
variable F : Π x, (Π y, r y x → C y) → C x

namespace well_founded

lemma fix_F_eq0 : fix_F F x acx = fix_F F x (acc.intro x $ λ y, acx.inv) := rfl
lemma fix_F_eq1 : fix_F F x (acc.intro x $ λ y, acx.inv) = F x (λ y p, fix_F F y $ acx.inv p) := rfl
lemma fix_F_eq2 : fix_F F x acx = F x (λ y p, fix_F F y $ acx.inv p) := rfl
/- fix_F_eq2 fails but fix_F_eq0 and fix_F_eq1 work, demonstrating nontransitivity. -/

alreadydone

variables {α : Type*} (r : α → α → Prop) {a b c : α}

inductive eqv_gen' : α → α → Prop
| refl (a) : eqv_gen' a a
| transl {a b c} : eqv_gen' a b → r c b → eqv_gen' a c
| transr {a b c} : eqv_gen' a b → r b c → eqv_gen' a c

variable {r}

lemma eqv_gen'_rel (h : r a b) : eqv_gen' r a b := (eqv_gen'.refl a).transr h

alreadydone

import algebra.big_operators.fin
import algebra.big_operators.order
import data.nat.choose.basic
import data.finset.sym
import data.finsupp.multiset
import data.fin.vec_notation
import data.nat.choose.sum

open_locale nat big_operators

alreadydone

import data.mv_polynomial.basic
import tactic.fin_cases
import algebra.char_p.algebra

open mv_polynomial

variables (σ R : Type*) [comm_semiring R]

def ideal_ge (a : σ → ℕ) : ideal (mv_polynomial σ R) :=
{ carrier := {p | ∀ (m : σ →₀ ℕ), m ∈ p.support → ∃ i, a i ≤ m i},

alreadydone

import field_theory.is_alg_closed.basic
import logic.equiv.transfer_instance
import algebra.direct_limit

/-! Existence of algebraic closure via Zorn's lemma. We follow Zbigniew Jelonek's proof from
  https://math.stackexchange.com/a/621955/12932;
  also in GTM 167, *Field and Galois Theory* by Patrick Morandi. -/

universe u

alreadydone

import analysis.complex.polynomial
import field_theory.adjoin
import field_theory.is_alg_closed.basic

open_locale polynomial
open polynomial

constant p : ℚ[X]

noncomputable def K : intermediate_field ℚ ℂ :=