one_le_evenOdd_zero — Mathlib

English

The unit element 1 belongs to the even submodule at degree 0, i.e., 1 ≤ evenOdd Q 0 holds, reflecting that scalars lie in the even part.

Русский

Единица принадлежит четной подмодули на нулевой степени: 1 ≤ evenOdd Q 0, что соответствует размещению скаляров в четной части.

LaTeX

$$$1 \\le \\mathrm{evenOdd}_Q(0)$$$

Lean4

theorem one_le_evenOdd_zero : 1 ≤ evenOdd Q 0 :=
  by
  refine le_trans ?_ (le_iSup _ ⟨0, Nat.cast_zero⟩)
  exact (pow_zero _).ge

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