toDual_injective

Mathlib.LinearAlgebra.Dual.Basis

URI: https://scilib.ai/kg/mathlib#Module.Basis.toDual_injective

English

The map toDual is injective: if b.toDual m = b.toDual n, then m = n.

Русский

Отображение toDual инъективно: если b.toDual m = b.toDual n, то m = n.

LaTeX

$$$ \text{Injective}(b.toDual). $$$

Lean4

theorem toDual_injective : Injective b.toDual := fun x y h ↦
  b.ext_elem_iff.mpr fun i ↦ by simp_rw [← toDual_eq_repr]; exact DFunLike.congr_fun h _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru