mk'_eq_mk

Mathlib.LinearAlgebra.Projectivization.Basic

URI: https://scilib.ai/kg/mathlib#Projectivization.mk'_eq_mk

English

Equality between mk' and mk applied to representative.

Русский

Равенство mk' и mk применено к представителю.

LaTeX

$$$ \mathrm{mk}'(K,v) = \mathrm{mk}(K,v.1, v.2) $$$

Lean4

@[simp]
theorem mk'_eq_mk (v : { v : V // v ≠ 0 }) : mk' K v = mk K (↑v) v.2 :=
  rfl

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

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

Разделы

Аффилиация

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