NYLL
Module

Finrank_adjoin_eq_card_of_mul_mem_span_of_fractions.lean

Nyll.AlgebraicCurves.FunctionFields.Finrank_adjoin_eq_card_of_mul_mem_span_of_fractions
6 declarations indexed from sourceView source ↗

Module documentation

Finrank adjoin eq card of mul mem span of fractions

Imports7
  • Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
  • Mathlib.RingTheory.Localization.Module
  • Mathlib.LinearAlgebra.FiniteDimensional.Basic
  • Mathlib.LinearAlgebra.Dimension.StrongRankCondition
  • Mathlib.Tactic.Choose
  • Mathlib.Tactic.Ring.RingNF
  • Mathlib.Tactic.FieldSimp
Imported by1

Declarations

theorem

aeval_mem_adjoin

L39 ↗
AlgebraicCurves.FunctionFields.Proofs.Finrank_adjoin_eq_card_of_mul_mem_span_of_fractions.AlgebraicCurve.FinrankOrder.aeval_mem_adjoin
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finrank_adjoin_eq_card_of_mul_mem_span_of_fractions
open Polynomial
universe u v
namespace AlgebraicCurve
namespace FinrankOrder
variable {k : Type u} {E : Type v} [Field k] [Field E] [Algebra k E] {n : ℕ}
  (y : E) (s : Fin n → E)
Lean source · statement
theorem aeval_mem_adjoin (c : k[X]) :
    Polynomial.aeval y c ∈ IntermediateField.adjoin k ({y} : Set E)
theorem

linearIndependent_algebraAdjoin

L45 ↗
AlgebraicCurves.FunctionFields.Proofs.Finrank_adjoin_eq_card_of_mul_mem_span_of_fractions.AlgebraicCurve.FinrankOrder.linearIndependent_algebraAdjoin
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finrank_adjoin_eq_card_of_mul_mem_span_of_fractions
open Polynomial
universe u v
namespace AlgebraicCurve
namespace FinrankOrder
variable {k : Type u} {E : Type v} [Field k] [Field E] [Algebra k E] {n : ℕ}
  (y : E) (s : Fin n → E)
Lean source · statement
theorem linearIndependent_algebraAdjoin
    (hind : ∀ c : Fin n → k[X], ∑ i, Polynomial.aeval y (c i) * s i = 0 → c = 0) :
    LinearIndependent (Algebra.adjoin k ({y} : Set E)) s
theorem

linearIndependent_adjoin

L65 ↗
AlgebraicCurves.FunctionFields.Proofs.Finrank_adjoin_eq_card_of_mul_mem_span_of_fractions.AlgebraicCurve.FinrankOrder.linearIndependent_adjoin
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finrank_adjoin_eq_card_of_mul_mem_span_of_fractions
open Polynomial
universe u v
namespace AlgebraicCurve
namespace FinrankOrder
variable {k : Type u} {E : Type v} [Field k] [Field E] [Algebra k E] {n : ℕ}
  (y : E) (s : Fin n → E)
open scoped IntermediateField.algebraAdjoinAdjoin in
Lean source · statement
theorem linearIndependent_adjoin
    (hind : ∀ c : Fin n → k[X], ∑ i, Polynomial.aeval y (c i) * s i = 0 → c = 0) :
    LinearIndependent (IntermediateField.adjoin k ({y} : Set E)) s
theorem

mul_mem_span

L71 ↗
AlgebraicCurves.FunctionFields.Proofs.Finrank_adjoin_eq_card_of_mul_mem_span_of_fractions.AlgebraicCurve.FinrankOrder.mul_mem_span
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finrank_adjoin_eq_card_of_mul_mem_span_of_fractions
open Polynomial
universe u v
namespace AlgebraicCurve
namespace FinrankOrder
variable {k : Type u} {E : Type v} [Field k] [Field E] [Algebra k E] {n : ℕ}
  (y : E) (s : Fin n → E)
Lean source · statement
theorem mul_mem_span
    (hmul : ∀ i j, ∃ c : Fin n → k[X], s i * s j = ∑ l, Polynomial.aeval y (c l) * s l)
    {a b : E}
    (ha : a ∈ Submodule.span (IntermediateField.adjoin k ({y} : Set E)) (Set.range s))
    (hb : b ∈ Submodule.span (IntermediateField.adjoin k ({y} : Set E)) (Set.range s)) :
    a * b ∈ Submodule.span (IntermediateField.adjoin k ({y} : Set E)) (Set.range s)
theorem

span_eq_top

L98 ↗
AlgebraicCurves.FunctionFields.Proofs.Finrank_adjoin_eq_card_of_mul_mem_span_of_fractions.AlgebraicCurve.FinrankOrder.span_eq_top
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finrank_adjoin_eq_card_of_mul_mem_span_of_fractions
open Polynomial
universe u v
namespace AlgebraicCurve
namespace FinrankOrder
variable {k : Type u} {E : Type v} [Field k] [Field E] [Algebra k E] {n : ℕ}
  (y : E) (s : Fin n → E)
Lean source · statement
theorem span_eq_top
    (hmul : ∀ i j, ∃ c : Fin n → k[X], s i * s j = ∑ l, Polynomial.aeval y (c l) * s l)
    (hfrac : ∀ z : E, ∃ cu cv : Fin n → k[X],
      ∑ i, Polynomial.aeval y (cv i) * s i ≠ 0 ∧
        z * ∑ i, Polynomial.aeval y (cv i) * s i = ∑ i, Polynomial.aeval y (cu i) * s i) :
    Submodule.span (IntermediateField.adjoin k ({y} : Set E)) (Set.range s) = ⊤
theorem

finrank_adjoin_eq_card_of_mul_mem_span_of_fractions

L159 ↗
AlgebraicCurve.finrank_adjoin_eq_card_of_mul_mem_span_of_fractions
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Finrank_adjoin_eq_card_of_mul_mem_span_of_fractions
open Polynomial
universe u v
open AlgebraicCurve.FinrankOrder in
Lean source · statement
theorem _root_.AlgebraicCurve.finrank_adjoin_eq_card_of_mul_mem_span_of_fractions
    {k : Type u} {E : Type v} [Field k] [Field E] [Algebra k E] {n : ℕ}
    (y : E) (s : Fin n → E)
    (hmul : ∀ i j, ∃ c : Fin n → k[X], s i * s j = ∑ l, Polynomial.aeval y (c l) * s l)
    (hind : ∀ c : Fin n → k[X], ∑ i, Polynomial.aeval y (c i) * s i = 0 → c = 0)
    (hfrac : ∀ z : E, ∃ cu cv : Fin n → k[X],
      ∑ i, Polynomial.aeval y (cv i) * s i ≠ 0 ∧
        z * ∑ i, Polynomial.aeval y (cv i) * s i = ∑ i, Polynomial.aeval y (cu i) * s i) :
    FiniteDimensional (IntermediateField.adjoin k ({y} : Set E)) E ∧
      Module.finrank (IntermediateField.adjoin k ({y} : Set E)) E = n

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.