toNNReal_ne_zero

Mathlib.Data.Int.WithZero

URI: https://scilib.ai/kg/mathlib#WithZeroMulInt.toNNReal_ne_zero

← MathLib Explorer

English

If e ≠ 0 and m ≠ 0, then toNNReal e m ≠ 0.

Русский

Если e ≠ 0 и m ≠ 0, то toNNReal e m ≠ 0.

LaTeX

$$$\text{toNNReal } e\ m \neq 0$$$

Lean4

/-- `toNNReal` sends nonzero elements to nonzero elements. -/
theorem toNNReal_ne_zero {e : ℝ≥0} {m : ℤᵐ⁰} (he : e ≠ 0) (hm : m ≠ 0) : toNNReal he m ≠ 0 := by
  simp only [ne_eq, map_eq_zero, hm, not_false_eq_true]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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