def termVectorSpace : Lean.ParserDescr

Equations

• termVectorSpace = Lean.ParserDescr.node `termVectorSpace 1024 (Lean.ParserDescr.symbol "VectorSpace")

structure CoordinateSystem (F : Type u_1) (V : Type u_2) (P : Type u_3) [Field F] [AddCommGroup V] [VectorSpace F V] [AddTorsor V P] : Type (max (max (max 1 u_1) u_2) u_3)

• ι : Type
• origin : P
• basis : Module.Basis self.ι F V

def CoordinateSystem.coordinates {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [VectorSpace F V] {P : Type u_3} [AddTorsor V P] (cs : CoordinateSystem F V P) (p : P) : cs.ι → F

Equations

• cs.coordinates p = ⇑(cs.basis.repr (p -ᵥ cs.origin))

structure PolynomialMapInCoords {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [VectorSpace F V] {P : Type u_3} [AddTorsor V P] {W : Type u_4} [AddCommGroup W] [VectorSpace F W] {R : Type u_5} [AddTorsor W R] (map : P → R) (cs₁ : CoordinateSystem F V P) (cs₂ : CoordinateSystem F W R) : Type u_1

• polys : cs₂.ι → MvPolynomial cs₁.ι F
• map_poly_eq (p : P) (i : cs₂.ι) : cs₂.coordinates (map p) i = (MvPolynomial.eval (cs₁.coordinates p)) (self.polys i)
• degree : ℕ
• deg_max (i : cs₂.ι) : self.degree ≥ (self.polys i).totalDegree
• deg_exist : ∃ (i : cs₂.ι), self.degree = (self.polys i).totalDegree

def isPolyMapInCoords {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [VectorSpace F V] {P : Type u_3} [AddTorsor V P] {W : Type u_4} [AddCommGroup W] [VectorSpace F W] {R : Type u_5} [AddTorsor W R] (map : P → R) (cs₁ : CoordinateSystem F V P) (cs₂ : CoordinateSystem F W R) : Prop

Equations

• isPolyMapInCoords map cs₁ cs₂ = Nonempty (PolynomialMapInCoords map cs₁ cs₂)

theorem poly_in_one_poly_in_another {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [VectorSpace F V] {P : Type u_3} [AddTorsor V P] {W : Type u_4} [AddCommGroup W] [VectorSpace F W] {R : Type u_5} [AddTorsor W R] (map : P → R) (cs₁ : CoordinateSystem F V P) (cs₂ : CoordinateSystem F W R) (cs₃ : CoordinateSystem F V P) (cs₄ : CoordinateSystem F W R) : isPolyMapInCoords map cs₁ cs₂ → isPolyMapInCoords map cs₃ cs₄

theorem poly_in_one_poly_in_all {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [VectorSpace F V] {P : Type u_3} [AddTorsor V P] {W : Type u_4} [AddCommGroup W] [VectorSpace F W] {R : Type u_5} [AddTorsor W R] (map : P → R) (cs₁ : CoordinateSystem F V P) (cs₂ : CoordinateSystem F W R) : isPolyMapInCoords map cs₁ cs₂ → ∀ (cs₃ : CoordinateSystem F V P) (cs₄ : CoordinateSystem F W R), isPolyMapInCoords map cs₃ cs₄

def isPolyMap {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [VectorSpace F V] {P : Type u_3} [AddTorsor V P] {W : Type u_4} [AddCommGroup W] [VectorSpace F W] {R : Type u_5} [AddTorsor W R] (map : P → R) : Prop

Equations

• isPolyMap map = ∃ (cs₁ : CoordinateSystem F V P) (cs₂ : CoordinateSystem F W R), isPolyMapInCoords map cs₁ cs₂