X_inj — Mathlib

English

The indeterminates X_s are all distinct: X_s = X_t if and only if s = t (for a nontrivial coefficient ring).

Русский

Индетерминанты X_s различны: X_s = X_t тогда и только тогда, когда s = t.

LaTeX

$$$X_s = X_t \\iff s = t$$$

Lean4

theorem X_inj [Nontrivial R] {s t : σ} : (X s : MvPowerSeries σ R) = X t ↔ s = t :=
  ⟨by
    classical
    intro h
    replace h := congr_arg (coeff (single s 1)) h
    rw [coeff_X, if_pos rfl, coeff_X] at h
    split_ifs at h with H
    · rw [Finsupp.single_eq_single_iff] at H
      rcases H with H | H
      · exact H.1
      · exfalso
        exact one_ne_zero H.1
    · exfalso
      exact one_ne_zero h,
    congr_arg X⟩

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