subsingleton — Mathlib

English

If CharP R 1 holds, then R is a Subsingleton.

Русский

Если CharP R 1 выполняется, то R является subsingleton.

LaTeX

$$[CharP R 1] ⇒ Subsingleton R$$

Lean4

theorem subsingleton [CharP R 1] : Subsingleton R :=
  Subsingleton.intro <|
    suffices ∀ r : R, r = 0 from fun a b => show a = b by rw [this a, this b]
    fun r =>
    calc
      r = 1 * r := by rw [one_mul]
      _ = (1 : ℕ) * r := by rw [Nat.cast_one]
      _ = 0 * r := by rw [CharP.cast_eq_zero]
      _ = 0 := by rw [zero_mul]

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