coe_inj — Mathlib

English

The coercion is injective; equality of underlying functions implies equality of alternating maps.

Русский

Умножение через приведение к функциям инъективно; равенство базовых функций влечет равенство чередующихся отображений.

LaTeX

$$∀ {R : Type*} [Semiring R] {M : Type*} [AddCommMonoid M] [Module R M] {ι : Type*} {f g : AlternatingMap R M N ι}, (f : (ι → M) → N) = g ↔ f = g$$

Lean4

@[norm_cast]
theorem coe_inj {f g : M [⋀^ι]→ₗ[R] N} : (f : (ι → M) → N) = g ↔ f = g :=
  coe_injective.eq_iff

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