Nyll.AlgebraicCurves.Places.Taylor.IsConfluentPattern_exists_eq_of_lt_jetMult

theorem

exists_eq_of_lt_jetMult

AlgebraicCurve.IsConfluentPattern.exists_eq_of_lt_jetMult

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Taylor.Proofs.IsConfluentPattern_exists_eq_of_lt_jetMult
open AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.IsConfluentPattern.exists_eq_of_lt_jetMult
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    {M : ℕ} {P : Fin M → Place K F} {t : Fin M → F} {e : Fin M → ℕ}
    (hpat : IsConfluentPattern P t e) (i : Fin M) {q : ℕ} (hq : q < jetMult P (P i)) :
    ∃ i', P i' = P i ∧ e i' = q

IsConfluentPattern_exists_eq_of_lt_jetMult.lean

Module documentation

Is Confluent Pattern exists eq of lt jet Mult

exists_eq_of_lt_jetMult

Module documentation

Is Confluent Pattern exists eq of lt jet Mult

Declarations

exists_eq_of_lt_jetMult