smul_one_eq_cast

Mathlib.Algebra.Field.Defs

URI: https://scilib.ai/kg/mathlib#NNRat.smul_one_eq_cast

English

For any q ∈ ℚ≥0, q • 1_K equals q viewed as an element of K.

Русский

Для любого q ∈ ℚ≥0, q • 1_K равно q как элементу K.

LaTeX

$$$q \cdot 1_K = (q : K)$$$

Lean4

@[simp]
theorem smul_one_eq_cast (q : ℚ≥0) : q • (1 : K) = q := by rw [NNRat.smul_def, mul_one]

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

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

Разделы

Аффилиация

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