ext_elem — Mathlib

English

ext_elem asserts that h.ext_elem x y: equality follows from coordinate-wise equality.

Русский

ext_elem утверждает, что равенство элементов следует из покомпонентного равенства коэффициентов.

LaTeX

$$ext_elem$$

Lean4

theorem ext_elem ⦃x y : S⦄ (hxy : ∀ i < natDegree f, h.coeff x i = h.coeff y i) : x = y :=
  EquivLike.injective h.basis.equivFun <|
    funext fun i => by
      rw [Basis.equivFun_apply, ← h.coeff_apply_coe, Basis.equivFun_apply, ← h.coeff_apply_coe, hxy i i.prop]

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