fact_ramificationIdx_neZero — Mathlib

English

If P lies over p in a tower of algebras, and p ≠ ⊥, then ramificationIdx (algebraMap R S) p P ≠ 0.

Русский

Если P лежит над p в тензорном разложении и p ≠ ⊥, то рамификация ненулевая.

LaTeX

$$$\\\\operatorname{ramificationIdx} (\\\\text{algebraMap } R S) p P \\\\neq 0$$$

Lean4

instance fact_ramificationIdx_neZero (P : (factors (map (algebraMap R S) p)).toFinset) :
    NeZero (ramificationIdx (algebraMap R S) p P) :=
  ⟨Factors.ramificationIdx_ne_zero p P⟩

Похожие утверждения