ofFinsupp_inj — Mathlib

English

A variant of injectivity: (⟨a⟩) = ⟨b⟩ in SkewMonoidAlgebra k G iff a = b.

Русский

Вариант инъективности: (⟨а⟩) = ⟨b⟩ в SkewMonoidAlgebra k G тогда и только тогда, когда a = b.

LaTeX

$$$ (\langle a \rangle = \langle b \rangle) \iff a = b $$$

Lean4

/-- A variant of `SkewMonoidAlgebra.ofFinsupp_injective` in terms of `Iff`. -/
theorem ofFinsupp_inj {a b} : (⟨a⟩ : SkewMonoidAlgebra k G) = ⟨b⟩ ↔ a = b :=
  ofFinsupp_injective.eq_iff

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