natCast_def'

Mathlib.RingTheory.TensorProduct.Basic

URI: https://scilib.ai/kg/mathlib#Algebra.TensorProduct.natCast_def'

English

There is a symmetric variant: (n : A ⊗_R B) = 1 ⊗_tmul (n : B) for natural n.

Русский

Существует симметричная формула: (n : A ⊗_R B) = 1 ⊗_tmul (n : B).

LaTeX

$$$ (n : A \otimes_R B) = (1 : A) \otimes_\text{tmul} (n : B) \quad (n \in \mathbb{N}). $$$

Lean4

theorem natCast_def' (n : ℕ) : (n : A ⊗[R] B) = (1 : A) ⊗ₜ (n : B) := by
  rw [natCast_def, ← nsmul_one, smul_tmul, nsmul_one]

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

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

Разделы

Аффилиация

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