nontrivial — Mathlib

English

Under the hypothesis that p is prime and p is not a unit in O, the quotient ModP O p is nontrivial.

Русский

При предположении, что p — простое и не является единицей в O, фактор-множество ModP O p не тривиально.

LaTeX

$$$\mathrm{ModP}(O,p) \neq \{0,1\}$$$

Lean4

instance nontrivial [hp : Fact p.Prime] [Fact (¬IsUnit (p : O))] : Nontrivial (ModP O p) :=
  CharP.nontrivial_of_char_ne_one hp.1.ne_one

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