eq_zero_of_zero_eq_one

Mathlib.Algebra.Module.Defs

URI: https://scilib.ai/kg/mathlib#Module.eq_zero_of_zero_eq_one

English

If (0 : R) = 1 in a semiring R, then for every x ∈ M we have x = 0.

Русский

Если в полугруппе R нулевой элемент равен единице, то для каждого элемента x модуля M выполняется x = 0.

LaTeX

$$$(0 : R) = 1 \\Rightarrow \\forall x \\in M,\ x = 0$$$

Lean4

theorem eq_zero_of_zero_eq_one (zero_eq_one : (0 : R) = 1) : x = 0 := by rw [← one_smul R x, ← zero_eq_one, zero_smul]

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

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

Разделы

Аффилиация

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