rootSpan_ne_bot — Mathlib

English

Let P be a RootPairing with data expressed over a type S and index set ι, under the standard hypotheses that S-modules M are nontrivial and ι is nonempty with 2 invertible in R. Then the root span P.rootSpan S is a nonzero submodule.

Русский

Пусть P — пары корней с данными над множеством индексов ι. При стандартных предположениях, что M является S-модулем и ι непусто, а 2 обратимо в R, то корневой охват P.rootSpan S не тождественно нулевой подпространство.

LaTeX

$$$P{\cdot}rootSpan{S} \neq \bot$$$

Lean4

theorem rootSpan_ne_bot [Module S M] [Nonempty ι] [NeZero (2 : R)] : P.rootSpan S ≠ ⊥ := by
  simpa [rootSpan] using P.exists_ne_zero

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