scalar_inj — Mathlib

English

If the index type n is nonempty, then the map r ↦ scalar n r is injective: for any r,s ∈ α, scalar n r = scalar n s implies r = s.

Русский

Пусть n непусто. Тогда отображение r ↦ scalar n r инъективно: для любых r,s ∈ α, если scalar n r = scalar n s, то r = s.

LaTeX

$$\text{If } \text{Nonempty}(n) \text{ then } scalar(n)(r) = scalar(n)(s) \iff r = s$$

Lean4

theorem scalar_inj [Nonempty n] {r s : α} : scalar n r = scalar n s ↔ r = s :=
  (diagonal_injective.comp Function.const_injective).eq_iff

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