AlgebraicCurve.Place.taylorRem_succ_eq_taylorRem_taylorRem_one
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_taylorRem_succ_eq_taylorRem_taylorRem_one
open AlgebraicCurve AlgebraicCurve.PlaceLean source · statement
theorem _root_.AlgebraicCurve.Place.taylorRem_succ_eq_taylorRem_taylorRem_one
{K F : Type*} [Field K] [Field F] [Algebra K F]
(v : Place K F) (t f : F) (r : ℕ) :
taylorRem v t f (r + 1) = taylorRem v t (taylorRem v t f 1) r