smul_one_eq_cast

Mathlib.Algebra.Module.NatInt

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

English

For any NonAssocSemiring R, and any natural m, m • 1_R equals the cast of m in R, i.e., m • 1_R = (m : R).

Русский

Для любого NonAssocSemiring R и любого натурального m выполняется m • 1_R = (m : R).

LaTeX

$$$\\forall m \\in \\mathbb{N},\\ m \\cdot 1_R = (m : R)$$$

Lean4

theorem smul_one_eq_cast {R : Type*} [NonAssocSemiring R] (m : ℕ) : m • (1 : R) = ↑m := by rw [nsmul_eq_mul, mul_one]

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

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

Разделы

Аффилиация

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