instNontrivialValueGroup — Mathlib

English

ValueGroup(A,K) is nontrivial; there exist 0 ≠ 1 in ValueGroup(A,K).

Русский

ValueGroup(A,K) ненулева; существуют 0 и 1, не совпадающие.

LaTeX

$$Nontrivial (ValueGroup(A,K)); exists 0 ≠ 1 in ValueGroup(A,K).$$

Lean4

instance : Nontrivial (ValueGroup A K) where
  exists_pair_ne :=
    ⟨0, 1, fun c => by
      obtain ⟨d, hd⟩ := Quotient.exact' c
      apply_fun fun t => d⁻¹ • t at hd
      dsimp at hd
      simp only [inv_smul_smul, smul_zero, one_ne_zero] at hd⟩

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