ne_neg — Mathlib

English

Under appropriate domain and finiteness assumptions, i ≠ -i for every i in ι; more precisely, with 2 nonzero and domain conditions, i ≠ -i.

Русский

При заданных условиях домена и конечности, для каждого i ∈ ι верно i ≠ -i; точнее при 2≠0 и домене, i ≠ -i.

LaTeX

$$$ i \neq -i $$$

Lean4

theorem ne_neg [NeZero (2 : R)] [IsDomain R] :
    letI := P.indexNeg
    i ≠ -i :=
  by
  have := Module.IsReflexive.of_isPerfPair P.toLinearMap
  intro contra
  replace contra : P.root i = -P.root i := by simpa using congr_arg P.root contra
  simp [eq_neg_iff_add_eq_zero, ← two_smul R, NeZero.out, P.ne_zero i] at contra

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