mult_coe_ne_zero

Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.InfinitePlace.mult_coe_ne_zero

English

The real cast of mult w is nonzero: (mult w : ℝ) ≠ 0.

Русский

Образ множителя в ℝ не равен нулю: (mult w : ℝ) ≠ 0.

LaTeX

$$$\forall w : \mathrm{InfinitePlace} K, (\operatorname{mult}(w) : \mathbb{R}) \neq 0$$$

Lean4

theorem mult_coe_ne_zero {w : InfinitePlace K} : (mult w : ℝ) ≠ 0 :=
  Nat.cast_ne_zero.mpr mult_ne_zero

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

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

Разделы

Аффилиация

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