card_pos — Mathlib

English

For an arithmetic Frobenius endomorphism φ with respect to Q, the corresponding quotient has a positive cardinality.

Русский

Для арифметического Фробениуса φ относительно идеала Q кардинализация соответствующего квотиона положительна.

LaTeX

$$$0 < \operatorname{card}(R/ Q.under R)$$$

Lean4

theorem card_pos : 0 < Nat.card (R ⧸ Q.under R) :=
  have := H.finite_quotient
  Nat.card_pos

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