uniqueLeft

Mathlib.LinearAlgebra.TensorProduct.Basic

URI: https://scilib.ai/kg/mathlib#TensorProduct.uniqueLeft

Lean4

instance uniqueLeft [Subsingleton M] : Unique (M ⊗[R] N)
    where
  default := 0
  uniq
    z :=
    z.induction_on rfl (fun x y ↦ by rw [Subsingleton.elim x 0, zero_tmul]) <| by rintro _ _ rfl rfl; apply add_zero

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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