continuum_mul_nat

Mathlib.SetTheory.Cardinal.Continuum

URI: https://scilib.ai/kg/mathlib#Cardinal.continuum_mul_nat

English

For n ≠ 0, 𝔠 * n = 𝔠.

Русский

Для n ≠ 0: 𝔠 · n = 𝔠.

LaTeX

$$$\text{For } n \neq 0:\; \mathfrak{c} \cdot n = \mathfrak{c}$$$

Lean4

@[simp]
theorem continuum_mul_nat {n : ℕ} (hn : n ≠ 0) : 𝔠 * n = 𝔠 :=
  (mul_comm _ _).trans (nat_mul_continuum hn)

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

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

Разделы

Аффилиация

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