NYLL
Module

Place_taylorCoeff_succ_eq_taylorCoeff_taylorRem_one.lean

Nyll.AlgebraicCurves.Places.Place_taylorCoeff_succ_eq_taylorCoeff_taylorRem_one
1 declaration indexed from sourceView source ↗

Module documentation

Place taylor Coeff succ eq taylor Coeff taylor Rem one

Imports2
Imported by4

Declarations

theorem

taylorCoeff_succ_eq_taylorCoeff_taylorRem_one

L26 ↗
AlgebraicCurve.Place.taylorCoeff_succ_eq_taylorCoeff_taylorRem_one
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_taylorCoeff_succ_eq_taylorCoeff_taylorRem_one
open AlgebraicCurve AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.taylorCoeff_succ_eq_taylorCoeff_taylorRem_one
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) (t f : F) (r : ℕ) :
    taylorCoeff v t (r + 1) f = taylorCoeff v t r (taylorRem v t f 1)

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