ext_iff — Mathlib

English

Two elements p and q in SkewMonoidAlgebra k G are equal iff all their coefficients agree: p = q ⇔ ∀ n, p.coeff(n) = q.coeff(n).

Русский

Два элемента p и q в SkewMonoidAlgebra k G равны тогда и только тогда, когда их коэффициенты совпадают для всех n: p = q ⇔ ∀ n, p.coeff(n) = q.coeff(n).

LaTeX

$$$ p = q \iff \forall n, p.\mathrm{coeff}(n) = q.\mathrm{coeff}(n) $$$

Lean4

theorem ext_iff {p q : SkewMonoidAlgebra k G} : p = q ↔ ∀ n, coeff p n = coeff q n :=
  by
  rcases p with ⟨f : G →₀ k⟩
  rcases q with ⟨g : G →₀ k⟩
  simpa [coeff] using DFunLike.ext_iff (f := f) (g := g)

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