one_le_coe

Mathlib.Algebra.Order.GroupWithZero.Canonical

URI: https://scilib.ai/kg/mathlib#WithZero.one_le_coe

English

WithZero α respects the order with 1: 1 ≤ (a : WithZero α) iff 1 ≤ a.

Русский

WithZero α сохраняет порядок с единицей: 1 ≤ (a : WithZero α) ⇔ 1 ≤ a.

LaTeX

$$$ 1 \le (a : \mathrm{WithZero} \alpha) \iff 1 \le a $$$

Lean4

@[simp, norm_cast]
theorem one_le_coe [One α] : 1 ≤ (a : WithZero α) ↔ 1 ≤ a :=
  coe_le_coe

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

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

Разделы

Аффилиация

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